epii

Description: Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	isepi.b	$⊢ B = {Base}_{C}$
	isepi.h	$⊢ H = Hom (C)$
	isepi.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	isepi.e	$⊢ E = Epi (C)$
	isepi.c	$⊢ φ \to C \in Cat$
	isepi.x	$⊢ φ \to X \in B$
	isepi.y	$⊢ φ \to Y \in B$
	epii.z	$⊢ φ \to Z \in B$
	epii.f	$⊢ φ \to F \in (X E Y)$
	epii.g	$⊢ φ \to G \in (Y H Z)$
	epii.k	$⊢ φ \to K \in (Y H Z)$
Assertion	epii	$⊢ φ \to (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = K (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \leftrightarrow G = K)$

Proof

Step	Hyp	Ref	Expression
1		isepi.b	$⊢ B = {Base}_{C}$
2		isepi.h	$⊢ H = Hom (C)$
3		isepi.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		isepi.e	$⊢ E = Epi (C)$
5		isepi.c	$⊢ φ \to C \in Cat$
6		isepi.x	$⊢ φ \to X \in B$
7		isepi.y	$⊢ φ \to Y \in B$
8		epii.z	$⊢ φ \to Z \in B$
9		epii.f	$⊢ φ \to F \in (X E Y)$
10		epii.g	$⊢ φ \to G \in (Y H Z)$
11		epii.k	$⊢ φ \to K \in (Y H Z)$
12		eqid	$⊢ oppCat (C) = oppCat (C)$
13	1 3 12 8 7 6	oppcco	$⊢ φ \to F (⟨Z, Y⟩ comp (oppCat (C)) X) G = G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
14	1 3 12 8 7 6	oppcco	$⊢ φ \to F (⟨Z, Y⟩ comp (oppCat (C)) X) K = K (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
15	13 14	eqeq12d	$⊢ φ \to (F (⟨Z, Y⟩ comp (oppCat (C)) X) G = F (⟨Z, Y⟩ comp (oppCat (C)) X) K \leftrightarrow G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = K (⟨X, Y⟩ \underset{˙}{\cdot} Z) F)$
16	12 1	oppcbas	$⊢ B = {Base}_{oppCat (C)}$
17		eqid	$⊢ Hom (oppCat (C)) = Hom (oppCat (C))$
18		eqid	$⊢ comp (oppCat (C)) = comp (oppCat (C))$
19		eqid	$⊢ Mono (oppCat (C)) = Mono (oppCat (C))$
20	12	oppccat	$⊢ C \in Cat \to oppCat (C) \in Cat$
21	5 20	syl	$⊢ φ \to oppCat (C) \in Cat$
22	12 5 19 4	oppcmon	$⊢ φ \to Y Mono (oppCat (C)) X = X E Y$
23	9 22	eleqtrrd	$⊢ φ \to F \in (Y Mono (oppCat (C)) X)$
24	2 12	oppchom	$⊢ Z Hom (oppCat (C)) Y = Y H Z$
25	10 24	eleqtrrdi	$⊢ φ \to G \in (Z Hom (oppCat (C)) Y)$
26	11 24	eleqtrrdi	$⊢ φ \to K \in (Z Hom (oppCat (C)) Y)$
27	16 17 18 19 21 7 6 8 23 25 26	moni	$⊢ φ \to (F (⟨Z, Y⟩ comp (oppCat (C)) X) G = F (⟨Z, Y⟩ comp (oppCat (C)) X) K \leftrightarrow G = K)$
28	15 27	bitr3d	$⊢ φ \to (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = K (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \leftrightarrow G = K)$

Metamath Proof Explorer

Theorem epii

Proof