Theorem thincmon

Description: In a thin category, all morphisms are monomorphisms. The converse does not hold. See grptcmon . (Contributed by Zhi Wang, 24-Sep-2024)

	Ref	Expression
Hypotheses	thincid.c	|- ( ph -> C e. ThinCat )
	thincid.b	|- B = ( Base ` C )
	thincid.h	|- H = ( Hom ` C )
	thincid.x	|- ( ph -> X e. B )
	thincmon.y	|- ( ph -> Y e. B )
	thincmon.m	|- M = ( Mono ` C )
Assertion	thincmon	|- ( ph -> ( X M Y ) = ( X H Y ) )

Proof

Step	Hyp	Ref	Expression
1		thincid.c	|- ( ph -> C e. ThinCat )
2		thincid.b	|- B = ( Base ` C )
3		thincid.h	|- H = ( Hom ` C )
4		thincid.x	|- ( ph -> X e. B )
5		thincmon.y	|- ( ph -> Y e. B )
6		thincmon.m	|- M = ( Mono ` C )
7		simpr1	|- ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> z e. B )
8	4	adantr	|- ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> X e. B )
9		simpr2	|- ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> g e. ( z H X ) )
10		simpr3	|- ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> h e. ( z H X ) )
11	1	adantr	|- ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> C e. ThinCat )
12	7 8 9 10 2 3 11	thincmo2	|- ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> g = h )
13	12	a1d	|- ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> ( ( f ( <. z , X >. ( comp ` C ) Y ) g ) = ( f ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) )
14	13	ralrimivvva	|- ( ph -> A. z e. B A. g e. ( z H X ) A. h e. ( z H X ) ( ( f ( <. z , X >. ( comp ` C ) Y ) g ) = ( f ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) )
15		eqid	|- ( comp ` C ) = ( comp ` C )
16	1	thinccd	|- ( ph -> C e. Cat )
17	2 3 15 6 16 4 5	ismon2	|- ( ph -> ( f e. ( X M Y ) <-> ( f e. ( X H Y ) /\ A. z e. B A. g e. ( z H X ) A. h e. ( z H X ) ( ( f ( <. z , X >. ( comp ` C ) Y ) g ) = ( f ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) ) ) )
18	14 17	mpbiran2d	|- ( ph -> ( f e. ( X M Y ) <-> f e. ( X H Y ) ) )
19	18	eqrdv	|- ( ph -> ( X M Y ) = ( X H Y ) )