ismon

Description: Definition of a monomorphism in a category. (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	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}))$

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	monfval	$⊢ φ \to M = (x \in B, y \in B ⟼ \{f \in (x H y) \| \forall z \in B Fun {(g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g)}^{-1}\})$
9		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
10		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
11	9 10	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x H y = X H Y$
12	9	oveq2d	$⊢ (φ \land (x = X \land y = Y)) \to z H x = z H X$
13	9	opeq2d	$⊢ (φ \land (x = X \land y = Y)) \to ⟨z, x⟩ = ⟨z, X⟩$
14	13 10	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to ⟨z, x⟩ \underset{˙}{\cdot} y = ⟨z, X⟩ \underset{˙}{\cdot} Y$
15	14	oveqd	$⊢ (φ \land (x = X \land y = Y)) \to f (⟨z, x⟩ \underset{˙}{\cdot} y) g = f (⟨z, X⟩ \underset{˙}{\cdot} Y) g$
16	12 15	mpteq12dv	$⊢ (φ \land (x = X \land y = Y)) \to (g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g) = (g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)$
17	16	cnveqd	$⊢ (φ \land (x = X \land y = Y)) \to {(g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g)}^{-1} = {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}$
18	17	funeqd	$⊢ (φ \land (x = X \land y = Y)) \to (Fun {(g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g)}^{-1} \leftrightarrow Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1})$
19	18	ralbidv	$⊢ (φ \land (x = X \land y = 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 Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1})$
20	11 19	rabeqbidv	$⊢ (φ \land (x = X \land y = Y)) \to \{f \in (x H y) \| \forall z \in B Fun {(g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g)}^{-1}\} = \{f \in (X H Y) \| \forall z \in B Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}\}$
21		ovex	$⊢ X H Y \in V$
22	21	rabex	$⊢ \{f \in (X H Y) \| \forall z \in B Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}\} \in V$
23	22	a1i	$⊢ φ \to \{f \in (X H Y) \| \forall z \in B Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}\} \in V$
24	8 20 6 7 23	ovmpod	$⊢ φ \to X M Y = \{f \in (X H Y) \| \forall z \in B Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}\}$
25	24	eleq2d	$⊢ φ \to (F \in (X M Y) \leftrightarrow F \in \{f \in (X H Y) \| \forall z \in B Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}\})$
26		oveq1	$⊢ f = F \to f (⟨z, X⟩ \underset{˙}{\cdot} Y) g = F (⟨z, X⟩ \underset{˙}{\cdot} Y) g$
27	26	mpteq2dv	$⊢ f = F \to (g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g) = (g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)$
28	27	cnveqd	$⊢ f = F \to {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1} = {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1}$
29	28	funeqd	$⊢ f = F \to (Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1} \leftrightarrow Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1})$
30	29	ralbidv	$⊢ f = F \to (\forall z \in B Fun {(g \in (z H X) ⟼ f (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1} \leftrightarrow \forall z \in B Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1})$
31	30	elrab	$⊢ F \in \{f \in (X H Y) \| \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 Fun {(g \in (z H X) ⟼ F (⟨z, X⟩ \underset{˙}{\cdot} Y) g)}^{-1})$
32	25 31	bitrdi	$⊢ φ \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}))$

Metamath Proof Explorer

Theorem ismon

Proof