equalizer and monomorphism

1. Proposition

Let 20231221-equalizer_and_monomorphism_760824120891fc757bc0445145b027d09b237baa.svg be a category

Then

Suppose there exists an object 20231221-equalizer_and_monomorphism_9453902b5544d418294ac20701cedecedad7f2aa.svg and morphisms such that

Then we get a commuting diagram

Hence especially 20231221-equalizer_and_monomorphism_ccda4f3d79b188d47d3d14d7b71cfcde42b0c6c3.svg with is a fork

and therefore by universal property, there exists a unique mediating morphism

Since both 20231221-equalizer_and_monomorphism_ef19fff6fc4b820df543ab51bea9aef2124b3f3c.svg make the diagram commute, we conclude, that by uniqueness

and thus 20231221-equalizer_and_monomorphism_aed1b93b0b9c6bcecbd7c4ccb9fbf0cad460f4c8.svg is a monomorphism