Theorem thincepi

Description: In a thin category, all morphisms are epimorphisms. The converse does not hold. See grptcepi . (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 )
	thincepi.e	|- E = ( Epi ` C )
Assertion	thincepi	|- ( ph -> ( X E 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		thincepi.e	|- E = ( Epi ` C )
7	5	adantr	|- ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> Y e. B )
8		simpr1	|- ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> z e. B )
9		simpr2	|- ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> g e. ( Y H z ) )
10		simpr3	|- ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> h e. ( Y H z ) )
11	1	adantr	|- ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> C e. ThinCat )
12	7 8 9 10 2 3 11	thincmo2	|- ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> g = h )
13	12	a1d	|- ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> ( ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( <. X , Y >. ( comp ` C ) z ) f ) -> g = h ) )
14	13	ralrimivvva	|- ( ph -> A. z e. B A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( <. X , Y >. ( comp ` C ) z ) f ) -> g = h ) )
15		eqid	|- ( comp ` C ) = ( comp ` C )
16	1	thinccd	|- ( ph -> C e. Cat )
17	2 3 15 6 16 4 5	isepi2	|- ( ph -> ( f e. ( X E Y ) <-> ( f e. ( X H Y ) /\ A. z e. B A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( <. X , Y >. ( comp ` C ) z ) f ) -> g = h ) ) ) )
18	14 17	mpbiran2d	|- ( ph -> ( f e. ( X E Y ) <-> f e. ( X H Y ) ) )
19	18	eqrdv	|- ( ph -> ( X E Y ) = ( X H Y ) )