ismon2

Description: Write out the monomorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	ismon.b	$⊢ B = {Base}_{C}$
	ismon.h	$⊢ H = Hom (C)$
	ismon.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	ismon.s	$⊢ M = Mono (C)$
	ismon.c	$⊢ φ \to C \in Cat$
	ismon.x	$⊢ φ \to X \in B$
	ismon.y	$⊢ φ \to Y \in B$
Assertion	ismon2	$⊢ φ \to (F \in (X M Y) \leftrightarrow (F \in (X H Y) \land \forall z \in B \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h)))$

Proof

Step	Hyp	Ref	Expression
1		ismon.b	$⊢ B = {Base}_{C}$
2		ismon.h	$⊢ H = Hom (C)$
3		ismon.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		ismon.s	$⊢ M = Mono (C)$
5		ismon.c	$⊢ φ \to C \in Cat$
6		ismon.x	$⊢ φ \to X \in B$
7		ismon.y	$⊢ φ \to Y \in B$
8	1 2 3 4 5 6 7	ismon	$⊢ φ \to (F \in (X M Y) \leftrightarrow (F \in (X H Y) \land \forall z \in B Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}))$
9	5	ad2antrr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (z H X))) \to C \in Cat$
10		simprl	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (z H X))) \to z \in B$
11	6	ad2antrr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (z H X))) \to X \in B$
12	7	ad2antrr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (z H X))) \to Y \in B$
13		simprr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (z H X))) \to g \in (z H X)$
14		simplr	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (z H X))) \to F \in (X H Y)$
15	1 2 3 9 10 11 12 13 14	catcocl	$⊢ ((φ \land F \in (X H Y)) \land (z \in B \land g \in (z H X))) \to F (⟨z, X⟩ \underset{˙}{\cdot} Y) g \in (z H Y)$
16	15	anassrs	$⊢ (((φ \land F \in (X H Y)) \land z \in B) \land g \in (z H X)) \to F (⟨z, X⟩ \underset{˙}{\cdot} Y) g \in (z H Y)$
17	16	ralrimiva	$⊢ ((φ \land F \in (X H Y)) \land z \in B) \to \forall g \in (z H X) F (⟨z, X⟩ \underset{˙}{\cdot} Y) g \in (z H Y)$
18		eqid	$⊢ (g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) = (g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)$
19	18	fmpt	$⊢ \forall g \in (z H X) F (⟨z, X⟩ \underset{˙}{\cdot} Y) g \in (z H Y) \leftrightarrow (g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) : z H X ⟶ z H Y$
20		df-f1	$⊢ (g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) : z H X \underset{1-1}{⟶} z H Y \leftrightarrow ((g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) : z H X ⟶ z H Y \land Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1})$
21	20	baib	$⊢ (g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) : z H X ⟶ z H Y \to ((g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) : z H X \underset{1-1}{⟶} z H Y \leftrightarrow Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1})$
22	19 21	sylbi	$⊢ \forall g \in (z H X) F (⟨z, X⟩ \underset{˙}{\cdot} Y) g \in (z H Y) \to ((g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) : z H X \underset{1-1}{⟶} z H Y \leftrightarrow Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1})$
23		oveq2	$⊢ g = h \to F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h$
24	18 23	f1mpt	$⊢ (g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) : z H X \underset{1-1}{⟶} z H Y \leftrightarrow (\forall g \in (z H X) F (⟨z, X⟩ \underset{˙}{\cdot} Y) g \in (z H Y) \land \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h))$
25	24	baib	$⊢ \forall g \in (z H X) F (⟨z, X⟩ \underset{˙}{\cdot} Y) g \in (z H Y) \to ((g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g) : z H X \underset{1-1}{⟶} z H Y \leftrightarrow \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h))$
26	22 25	bitr3d	$⊢ \forall g \in (z H X) F (⟨z, X⟩ \underset{˙}{\cdot} Y) g \in (z H Y) \to (Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1} \leftrightarrow \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h))$
27	17 26	syl	$⊢ ((φ \land F \in (X H Y)) \land z \in B) \to (Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1} \leftrightarrow \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h))$
28	27	ralbidva	$⊢ (φ \land F \in (X H Y)) \to (\forall z \in B Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1} \leftrightarrow \forall z \in B \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h))$
29	28	pm5.32da	$⊢ φ \to ((F \in (X H Y) \land \forall z \in B Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}) \leftrightarrow (F \in (X H Y) \land \forall z \in B \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h)))$
30	8 29	bitrd	$⊢ φ \to (F \in (X M Y) \leftrightarrow (F \in (X H Y) \land \forall z \in B \forall g \in (z H X) \forall h \in (z H X) (F (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) h \to g = h)))$

Metamath Proof Explorer

Theorem ismon2

Proof