isepi

Description: Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-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$
Assertion	isepi	$⊢ φ \to (F \in (X E Y) \leftrightarrow (F \in (X H Y) \land \forall z \in B Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1}))$

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		eqid	$⊢ oppCat (C) = oppCat (C)$
9	8 1	oppcbas	$⊢ B = {Base}_{oppCat (C)}$
10		eqid	$⊢ Hom (oppCat (C)) = Hom (oppCat (C))$
11		eqid	$⊢ comp (oppCat (C)) = comp (oppCat (C))$
12		eqid	$⊢ Mono (oppCat (C)) = Mono (oppCat (C))$
13	8	oppccat	$⊢ C \in Cat \to oppCat (C) \in Cat$
14	5 13	syl	$⊢ φ \to oppCat (C) \in Cat$
15	9 10 11 12 14 7 6	ismon	$⊢ φ \to (F \in (Y Mono (oppCat (C)) X) \leftrightarrow (F \in (Y Hom (oppCat (C)) X) \land \forall z \in B Fun {(g \in (z Hom (oppCat (C)) Y) ⟼ F (⟨z, Y⟩ comp (oppCat (C)) X) g)}^{-1}))$
16	8 5 12 4	oppcmon	$⊢ φ \to Y Mono (oppCat (C)) X = X E Y$
17	16	eleq2d	$⊢ φ \to (F \in (Y Mono (oppCat (C)) X) \leftrightarrow F \in (X E Y))$
18	2 8	oppchom	$⊢ Y Hom (oppCat (C)) X = X H Y$
19	18	a1i	$⊢ φ \to Y Hom (oppCat (C)) X = X H Y$
20	19	eleq2d	$⊢ φ \to (F \in (Y Hom (oppCat (C)) X) \leftrightarrow F \in (X H Y))$
21	2 8	oppchom	$⊢ z Hom (oppCat (C)) Y = Y H z$
22	21	a1i	$⊢ (φ \land z \in B) \to z Hom (oppCat (C)) Y = Y H z$
23		simpr	$⊢ (φ \land z \in B) \to z \in B$
24	7	adantr	$⊢ (φ \land z \in B) \to Y \in B$
25	6	adantr	$⊢ (φ \land z \in B) \to X \in B$
26	1 3 8 23 24 25	oppcco	$⊢ (φ \land z \in B) \to F (⟨z, Y⟩ comp (oppCat (C)) X) g = g (⟨X, Y⟩ \underset{˙}{\cdot} z) F$
27	22 26	mpteq12dv	$⊢ (φ \land z \in B) \to (g \in (z Hom (oppCat (C)) Y) ⟼ F (⟨z, Y⟩ comp (oppCat (C)) X) g) = (g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)$
28	27	cnveqd	$⊢ (φ \land z \in B) \to {(g \in (z Hom (oppCat (C)) Y) ⟼ F (⟨z, Y⟩ comp (oppCat (C)) X) g)}^{-1} = {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1}$
29	28	funeqd	$⊢ (φ \land z \in B) \to (Fun {(g \in (z Hom (oppCat (C)) Y) ⟼ F (⟨z, Y⟩ comp (oppCat (C)) X) g)}^{-1} \leftrightarrow Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1})$
30	29	ralbidva	$⊢ φ \to (\forall z \in B Fun {(g \in (z Hom (oppCat (C)) Y) ⟼ F (⟨z, Y⟩ comp (oppCat (C)) X) g)}^{-1} \leftrightarrow \forall z \in B Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1})$
31	20 30	anbi12d	$⊢ φ \to ((F \in (Y Hom (oppCat (C)) X) \land \forall z \in B Fun {(g \in (z Hom (oppCat (C)) Y) ⟼ F (⟨z, Y⟩ comp (oppCat (C)) X) g)}^{-1}) \leftrightarrow (F \in (X H Y) \land \forall z \in B Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1}))$
32	15 17 31	3bitr3d	$⊢ φ \to (F \in (X E Y) \leftrightarrow (F \in (X H Y) \land \forall z \in B Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1}))$

Metamath Proof Explorer

Theorem isepi

Proof