Metamath Proof Explorer

Theorem grptcepi

Description: All morphisms in a category converted from a group are epimorphisms. (Contributed by Zhi Wang, 23-Sep-2024)

Ref Expression
Hypotheses grptcmon.c 
|- ( ph -> C = ( MndToCat ` G ) )
grptcmon.g 
|- ( ph -> G e. Grp )
grptcmon.b 
|- ( ph -> B = ( Base ` C ) )
grptcmon.x 
|- ( ph -> X e. B )
grptcmon.y 
|- ( ph -> Y e. B )
grptcmon.h 
|- ( ph -> H = ( Hom ` C ) )
grptcepi.e 
|- ( ph -> E = ( Epi ` C ) )
Assertion grptcepi 
|- ( ph -> ( X E Y ) = ( X H Y ) )

Proof

Step Hyp Ref Expression
1 grptcmon.c 
 |-  ( ph -> C = ( MndToCat ` G ) )
2 grptcmon.g 
 |-  ( ph -> G e. Grp )
3 grptcmon.b 
 |-  ( ph -> B = ( Base ` C ) )
4 grptcmon.x 
 |-  ( ph -> X e. B )
5 grptcmon.y 
 |-  ( ph -> Y e. B )
6 grptcmon.h 
 |-  ( ph -> H = ( Hom ` C ) )
7 grptcepi.e 
 |-  ( ph -> E = ( Epi ` C ) )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
10 eqid 
 |-  ( comp ` C ) = ( comp ` C )
11 eqid 
 |-  ( Epi ` C ) = ( Epi ` C )
12 2 grpmndd 
 |-  ( ph -> G e. Mnd )
13 1 12 mndtccat 
 |-  ( ph -> C e. Cat )
14 4 3 eleqtrd 
 |-  ( ph -> X e. ( Base ` C ) )
15 5 3 eleqtrd 
 |-  ( ph -> Y e. ( Base ` C ) )
16 8 9 10 11 13 14 15 isepi2 
 |-  ( ph -> ( f e. ( X ( Epi ` C ) Y ) <-> ( f e. ( X ( Hom ` C ) Y ) /\ A. z e. ( Base ` C ) A. g e. ( Y ( Hom ` C ) z ) A. h e. ( Y ( Hom ` C ) z ) ( ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( <. X , Y >. ( comp ` C ) z ) f ) -> g = h ) ) ) )
17 1 ad2antrr 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> C = ( MndToCat ` G ) )
18 12 ad2antrr 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> G e. Mnd )
19 3 ad2antrr 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> B = ( Base ` C ) )
20 4 ad2antrr 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> X e. B )
21 5 ad2antrr 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> Y e. B )
22 simpr1 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> z e. ( Base ` C ) )
23 22 19 eleqtrrd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> z e. B )
24 eqidd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( comp ` C ) = ( comp ` C ) )
25 eqidd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( <. X , Y >. ( comp ` C ) z ) = ( <. X , Y >. ( comp ` C ) z ) )
26 17 18 19 20 21 23 24 25 mndtcco2 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( g ( +g ` G ) f ) )
27 17 18 19 20 21 23 24 25 mndtcco2 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( h ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( +g ` G ) f ) )
28 26 27 eqeq12d 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( <. X , Y >. ( comp ` C ) z ) f ) <-> ( g ( +g ` G ) f ) = ( h ( +g ` G ) f ) ) )
29 2 ad2antrr 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> G e. Grp )
30 simpr2 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> g e. ( Y ( Hom ` C ) z ) )
31 eqidd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( Hom ` C ) = ( Hom ` C ) )
32 17 18 19 21 23 31 mndtchom 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( Y ( Hom ` C ) z ) = ( Base ` G ) )
33 30 32 eleqtrd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> g e. ( Base ` G ) )
34 simpr3 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> h e. ( Y ( Hom ` C ) z ) )
35 34 32 eleqtrd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> h e. ( Base ` G ) )
36 simplr 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> f e. ( X ( Hom ` C ) Y ) )
37 17 18 19 20 21 31 mndtchom 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( X ( Hom ` C ) Y ) = ( Base ` G ) )
38 36 37 eleqtrd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> f e. ( Base ` G ) )
39 eqid 
 |-  ( Base ` G ) = ( Base ` G )
40 eqid 
 |-  ( +g ` G ) = ( +g ` G )
41 39 40 grprcan 
 |-  ( ( G e. Grp /\ ( g e. ( Base ` G ) /\ h e. ( Base ` G ) /\ f e. ( Base ` G ) ) ) -> ( ( g ( +g ` G ) f ) = ( h ( +g ` G ) f ) <-> g = h ) )
42 29 33 35 38 41 syl13anc 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( ( g ( +g ` G ) f ) = ( h ( +g ` G ) f ) <-> g = h ) )
43 28 42 bitrd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( <. X , Y >. ( comp ` C ) z ) f ) <-> g = h ) )
44 43 biimpd 
 |-  ( ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) /\ ( z e. ( Base ` C ) /\ g e. ( Y ( Hom ` C ) z ) /\ h e. ( Y ( Hom ` C ) z ) ) ) -> ( ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( <. X , Y >. ( comp ` C ) z ) f ) -> g = h ) )
45 44 ralrimivvva 
 |-  ( ( ph /\ f e. ( X ( Hom ` C ) Y ) ) -> A. z e. ( Base ` C ) A. g e. ( Y ( Hom ` C ) z ) A. h e. ( Y ( Hom ` C ) z ) ( ( g ( <. X , Y >. ( comp ` C ) z ) f ) = ( h ( <. X , Y >. ( comp ` C ) z ) f ) -> g = h ) )
46 16 45 mpbiran3d 
 |-  ( ph -> ( f e. ( X ( Epi ` C ) Y ) <-> f e. ( X ( Hom ` C ) Y ) ) )
47 46 eqrdv 
 |-  ( ph -> ( X ( Epi ` C ) Y ) = ( X ( Hom ` C ) Y ) )
48 7 oveqd 
 |-  ( ph -> ( X E Y ) = ( X ( Epi ` C ) Y ) )
49 6 oveqd 
 |-  ( ph -> ( X H Y ) = ( X ( Hom ` C ) Y ) )
50 47 48 49 3eqtr4d 
 |-  ( ph -> ( X E Y ) = ( X H Y ) )