monfval

Description: Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-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$
Assertion	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}\})$

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		fvexd	$⊢ c = C \to {Base}_{c} \in V$
7		fveq2	$⊢ c = C \to {Base}_{c} = {Base}_{C}$
8	7 1	eqtr4di	$⊢ c = C \to {Base}_{c} = B$
9		fvexd	$⊢ (c = C \land b = B) \to Hom (c) \in V$
10		simpl	$⊢ (c = C \land b = B) \to c = C$
11	10	fveq2d	$⊢ (c = C \land b = B) \to Hom (c) = Hom (C)$
12	11 2	eqtr4di	$⊢ (c = C \land b = B) \to Hom (c) = H$
13		simplr	$⊢ ((c = C \land b = B) \land h = H) \to b = B$
14		simpr	$⊢ ((c = C \land b = B) \land h = H) \to h = H$
15	14	oveqd	$⊢ ((c = C \land b = B) \land h = H) \to x h y = x H y$
16	14	oveqd	$⊢ ((c = C \land b = B) \land h = H) \to z h x = z H x$
17		simpll	$⊢ ((c = C \land b = B) \land h = H) \to c = C$
18	17	fveq2d	$⊢ ((c = C \land b = B) \land h = H) \to comp (c) = comp (C)$
19	18 3	eqtr4di	$⊢ ((c = C \land b = B) \land h = H) \to comp (c) = \underset{˙}{\cdot}$
20	19	oveqd	$⊢ ((c = C \land b = B) \land h = H) \to ⟨z, x⟩ comp (c) y = ⟨z, x⟩ \underset{˙}{\cdot} y$
21	20	oveqd	$⊢ ((c = C \land b = B) \land h = H) \to f (⟨z, x⟩ comp (c) y) g = f (⟨z, x⟩ \underset{˙}{\cdot} y) g$
22	16 21	mpteq12dv	$⊢ ((c = C \land b = B) \land h = H) \to (g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) y) g) = (g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g)$
23	22	cnveqd	$⊢ ((c = C \land b = B) \land h = H) \to {(g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) y) g)}^{-1} = {(g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g)}^{-1}$
24	23	funeqd	$⊢ ((c = C \land b = B) \land h = H) \to (Fun {(g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) y) g)}^{-1} \leftrightarrow Fun {(g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g)}^{-1})$
25	13 24	raleqbidv	$⊢ ((c = C \land b = B) \land h = H) \to (\forall z \in b Fun {(g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) y) g)}^{-1} \leftrightarrow \forall z \in B Fun {(g \in (z H x) ⟼ f (⟨z, x⟩ \underset{˙}{\cdot} y) g)}^{-1})$
26	15 25	rabeqbidv	$⊢ ((c = C \land b = B) \land h = H) \to \{f \in (x h y) \| \forall z \in b Fun {(g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) 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}\}$
27	13 13 26	mpoeq123dv	$⊢ ((c = C \land b = B) \land h = H) \to (x \in b, y \in b ⟼ \{f \in (x h y) \| \forall z \in b Fun {(g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) y) g)}^{-1}\}) = (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}\})$
28	9 12 27	csbied2	$⊢ (c = C \land b = B) \to ⦋ Hom (c) / h ⦌ (x \in b, y \in b ⟼ \{f \in (x h y) \| \forall z \in b Fun {(g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) y) g)}^{-1}\}) = (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}\})$
29	6 8 28	csbied2	$⊢ c = C \to ⦋ {Base}_{c} / b ⦌ ⦋ Hom (c) / h ⦌ (x \in b, y \in b ⟼ \{f \in (x h y) \| \forall z \in b Fun {(g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) y) g)}^{-1}\}) = (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}\})$
30		df-mon	$⊢ Mono = (c \in Cat ⟼ ⦋ {Base}_{c} / b ⦌ ⦋ Hom (c) / h ⦌ (x \in b, y \in b ⟼ \{f \in (x h y) \| \forall z \in b Fun {(g \in (z h x) ⟼ f (⟨z, x⟩ comp (c) y) g)}^{-1}\}))$
31	1	fvexi	$⊢ B \in V$
32	31 31	mpoex	$⊢ (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}\}) \in V$
33	29 30 32	fvmpt	$⊢ C \in Cat \to Mono (C) = (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}\})$
34	5 33	syl	$⊢ φ \to Mono (C) = (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}\})$
35	4 34	eqtrid	$⊢ φ \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}\})$

Metamath Proof Explorer

Theorem monfval

Proof