This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )