isepi2

Description: Write out the epimorphism property directly. (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	isepi2	$⊢ φ \to (F \in (X E Y) \leftrightarrow (F \in (X H Y) \land \forall z \in B \forall g \in (Y H z) \forall h \in (Y H z) (g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F \to g = h)))$

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	1 2 3 4 5 6 7	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}))$
9	5	ad2antrr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (Y H z))) \to C \in Cat$
10	6	ad2antrr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (Y H z))) \to X \in B$
11	7	ad2antrr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (Y H z))) \to Y \in B$
12		simprl	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (Y H z))) \to z \in B$
13		simplr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (Y H z))) \to F \in (X H Y)$
14		simprr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (Y H z))) \to g \in (Y H z)$
15	1 2 3 9 10 11 12 13 14	catcocl	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (Y H z))) \to g (⟨X, Y⟩ \underset{˙}{\cdot} z) F \in (X H z)$
16	15	anassrs	$⊢ (((φ \land F \in (X H Y)) \land z \in B) \land g \in (Y H z)) \to g (⟨X, Y⟩ \underset{˙}{\cdot} z) F \in (X H z)$
17	16	ralrimiva	$⊢ ((φ \land F \in (X H Y)) \land z \in B) \to \forall g \in (Y H z) g (⟨X, Y⟩ \underset{˙}{\cdot} z) F \in (X H z)$
18		eqid	$⊢ (g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) = (g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)$
19	18	fmpt	$⊢ \forall g \in (Y H z) g (⟨X, Y⟩ \underset{˙}{\cdot} z) F \in (X H z) \leftrightarrow (g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) : Y H z ⟶ X H z$
20		df-f1	$⊢ (g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) : Y H z \underset{1-1}{⟶} X H z \leftrightarrow ((g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) : Y H z ⟶ X H z \land Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1})$
21	20	baib	$⊢ (g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) : Y H z ⟶ X H z \to ((g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) : Y H z \underset{1-1}{⟶} X H z \leftrightarrow Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1})$
22	19 21	sylbi	$⊢ \forall g \in (Y H z) g (⟨X, Y⟩ \underset{˙}{\cdot} z) F \in (X H z) \to ((g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) : Y H z \underset{1-1}{⟶} X H z \leftrightarrow Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1})$
23		oveq1	$⊢ g = h \to g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F$
24	18 23	f1mpt	$⊢ (g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) : Y H z \underset{1-1}{⟶} X H z \leftrightarrow (\forall g \in (Y H z) g (⟨X, Y⟩ \underset{˙}{\cdot} z) F \in (X H z) \land \forall g \in (Y H z) \forall h \in (Y H z) (g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F \to g = h))$
25	24	baib	$⊢ \forall g \in (Y H z) g (⟨X, Y⟩ \underset{˙}{\cdot} z) F \in (X H z) \to ((g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F) : Y H z \underset{1-1}{⟶} X H z \leftrightarrow \forall g \in (Y H z) \forall h \in (Y H z) (g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F \to g = h))$
26	22 25	bitr3d	$⊢ \forall g \in (Y H z) g (⟨X, Y⟩ \underset{˙}{\cdot} z) F \in (X H z) \to (Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1} \leftrightarrow \forall g \in (Y H z) \forall h \in (Y H z) (g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F \to g = h))$
27	17 26	syl	$⊢ ((φ \land F \in (X H Y)) \land z \in B) \to (Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1} \leftrightarrow \forall g \in (Y H z) \forall h \in (Y H z) (g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F \to g = h))$
28	27	ralbidva	$⊢ (φ \land F \in (X H Y)) \to (\forall z \in B Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1} \leftrightarrow \forall z \in B \forall g \in (Y H z) \forall h \in (Y H z) (g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F \to g = h))$
29	28	pm5.32da	$⊢ φ \to ((F \in (X H Y) \land \forall z \in B Fun {(g \in (Y H z) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} z) F)}^{-1}) \leftrightarrow (F \in (X H Y) \land \forall z \in B \forall g \in (Y H z) \forall h \in (Y H z) (g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F \to g = h)))$
30	8 29	bitrd	$⊢ φ \to (F \in (X E Y) \leftrightarrow (F \in (X H Y) \land \forall z \in B \forall g \in (Y H z) \forall h \in (Y H z) (g (⟨X, Y⟩ \underset{˙}{\cdot} z) F = h (⟨X, Y⟩ \underset{˙}{\cdot} z) F \to g = h)))$

Metamath Proof Explorer

Theorem isepi2

Proof