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	$⊢ φ \to C = MndToCat (G)$
	grptcmon.g	$⊢ φ \to G \in Grp$
	grptcmon.b	$⊢ φ \to B = {Base}_{C}$
	grptcmon.x	$⊢ φ \to X \in B$
	grptcmon.y	$⊢ φ \to Y \in B$
	grptcmon.h	$⊢ φ \to H = Hom (C)$
	grptcepi.e	$⊢ φ \to E = Epi (C)$
Assertion	grptcepi	$⊢ φ \to X E Y = X H Y$

Proof

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

Metamath Proof Explorer

Theorem grptcepi

Proof