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 No typesetting found for |- ( ph -> C = ( MndToCat ` G ) ) with typecode |-
grptcmon.g ⊢ φ → G ∈ Grp
grptcmon.b ⊢ φ → B = Base C
grptcmon.x ⊢ φ → X ∈ B
grptcmon.y ⊢ φ → Y ∈ B
grptcmon.h ⊢ φ → H = Hom ⁡ C
grptcepi.e ⊢ φ → E = Epi ⁡ C
Assertion grptcepi ⊢ φ → X E Y = X H Y

Proof

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