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=BaseC
grptcmon.x ⊢φ→X∈B
grptcmon.y ⊢φ→Y∈B
grptcmon.h ⊢φ→H=Hom⁡C
grptcepi.e ⊢φ→E=Epi⁡C
Assertion grptcepi ⊢φ→XEY=XHY

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=BaseC
4 grptcmon.x ⊢φ→X∈B
5 grptcmon.y ⊢φ→Y∈B
6 grptcmon.h ⊢φ→H=Hom⁡C
7 grptcepi.e ⊢φ→E=Epi⁡C
8 eqid ⊢BaseC=BaseC
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∈BaseC
15 5 3 eleqtrd ⊢φ→Y∈BaseC
16 8 9 10 11 13 14 15 isepi2 ⊢φ→f∈XEpi⁡CY↔f∈XHom⁡CY∧∀z∈BaseC∀g∈YHom⁡Cz∀h∈YHom⁡CzgXYcomp⁡Czf=hXYcomp⁡Czf→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∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→G∈Mnd
19 3 ad2antrr ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→B=BaseC
20 4 ad2antrr ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→X∈B
21 5 ad2antrr ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→Y∈B
22 simpr1 ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→z∈BaseC
23 22 19 eleqtrrd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→z∈B
24 eqidd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→comp⁡C=comp⁡C
25 eqidd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→XYcomp⁡Cz=XYcomp⁡Cz
26 17 18 19 20 21 23 24 25 mndtcco2 ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→gXYcomp⁡Czf=g+Gf
27 17 18 19 20 21 23 24 25 mndtcco2 ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→hXYcomp⁡Czf=h+Gf
28 26 27 eqeq12d ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→gXYcomp⁡Czf=hXYcomp⁡Czf↔g+Gf=h+Gf
29 2 ad2antrr ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→G∈Grp
30 simpr2 ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→g∈YHom⁡Cz
31 eqidd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→Hom⁡C=Hom⁡C
32 17 18 19 21 23 31 mndtchom ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→YHom⁡Cz=BaseG
33 30 32 eleqtrd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→g∈BaseG
34 simpr3 ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→h∈YHom⁡Cz
35 34 32 eleqtrd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→h∈BaseG
36 simplr ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→f∈XHom⁡CY
37 17 18 19 20 21 31 mndtchom ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→XHom⁡CY=BaseG
38 36 37 eleqtrd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→f∈BaseG
39 eqid ⊢BaseG=BaseG
40 eqid ⊢+G=+G
41 39 40 grprcan ⊢G∈Grp∧g∈BaseG∧h∈BaseG∧f∈BaseG→g+Gf=h+Gf↔g=h
42 29 33 35 38 41 syl13anc ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→g+Gf=h+Gf↔g=h
43 28 42 bitrd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→gXYcomp⁡Czf=hXYcomp⁡Czf↔g=h
44 43 biimpd ⊢φ∧f∈XHom⁡CY∧z∈BaseC∧g∈YHom⁡Cz∧h∈YHom⁡Cz→gXYcomp⁡Czf=hXYcomp⁡Czf→g=h
45 44 ralrimivvva ⊢φ∧f∈XHom⁡CY→∀z∈BaseC∀g∈YHom⁡Cz∀h∈YHom⁡CzgXYcomp⁡Czf=hXYcomp⁡Czf→g=h
46 16 45 mpbiran3d ⊢φ→f∈XEpi⁡CY↔f∈XHom⁡CY
47 46 eqrdv ⊢φ→XEpi⁡CY=XHom⁡CY
48 7 oveqd ⊢φ→XEY=XEpi⁡CY
49 6 oveqd ⊢φ→XHY=XHom⁡CY
50 47 48 49 3eqtr4d ⊢φ→XEY=XHY