fthmon

Description: A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fthmon.b	$⊢ B = {Base}_{C}$
	fthmon.h	$⊢ H = Hom (C)$
	fthmon.f	$⊢ φ \to F (C Faith D) G$
	fthmon.x	$⊢ φ \to X \in B$
	fthmon.y	$⊢ φ \to Y \in B$
	fthmon.r	$⊢ φ \to R \in (X H Y)$
	fthmon.m	$⊢ M = Mono (C)$
	fthmon.n	$⊢ N = Mono (D)$
	fthmon.1	$⊢ φ \to (X G Y) (R) \in (F (X) N F (Y))$
Assertion	fthmon	$⊢ φ \to R \in (X M Y)$

Proof

Step	Hyp	Ref	Expression
1		fthmon.b	$⊢ B = {Base}_{C}$
2		fthmon.h	$⊢ H = Hom (C)$
3		fthmon.f	$⊢ φ \to F (C Faith D) G$
4		fthmon.x	$⊢ φ \to X \in B$
5		fthmon.y	$⊢ φ \to Y \in B$
6		fthmon.r	$⊢ φ \to R \in (X H Y)$
7		fthmon.m	$⊢ M = Mono (C)$
8		fthmon.n	$⊢ N = Mono (D)$
9		fthmon.1	$⊢ φ \to (X G Y) (R) \in (F (X) N F (Y))$
10		eqid	$⊢ {Base}_{D} = {Base}_{D}$
11		eqid	$⊢ Hom (D) = Hom (D)$
12		eqid	$⊢ comp (D) = comp (D)$
13		fthfunc	$⊢ C Faith D \subseteq C Func D$
14	13	ssbri	$⊢ F (C Faith D) G \to F (C Func D) G$
15	3 14	syl	$⊢ φ \to F (C Func D) G$
16		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
17	15 16	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
18		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
19	17 18	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
20	19	simprd	$⊢ φ \to D \in Cat$
21	20	adantr	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to D \in Cat$
22	15	adantr	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to F (C Func D) G$
23	1 10 22	funcf1	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to F : B ⟶ {Base}_{D}$
24	4	adantr	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to X \in B$
25	23 24	ffvelrnd	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to F (X) \in {Base}_{D}$
26	5	adantr	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to Y \in B$
27	23 26	ffvelrnd	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to F (Y) \in {Base}_{D}$
28		simpr1	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to z \in B$
29	23 28	ffvelrnd	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to F (z) \in {Base}_{D}$
30	9	adantr	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to (X G Y) (R) \in (F (X) N F (Y))$
31	1 2 11 22 28 24	funcf2	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to (z G X) : z H X ⟶ F (z) Hom (D) F (X)$
32		simpr2	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to f \in (z H X)$
33	31 32	ffvelrnd	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to (z G X) (f) \in (F (z) Hom (D) F (X))$
34		simpr3	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to g \in (z H X)$
35	31 34	ffvelrnd	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to (z G X) (g) \in (F (z) Hom (D) F (X))$
36	10 11 12 8 21 25 27 29 30 33 35	moni	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to ((X G Y) (R) (⟨F (z), F (X)⟩ comp (D) F (Y)) (z G X) (f) = (X G Y) (R) (⟨F (z), F (X)⟩ comp (D) F (Y)) (z G X) (g) \leftrightarrow (z G X) (f) = (z G X) (g))$
37		eqid	$⊢ comp (C) = comp (C)$
38	6	adantr	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to R \in (X H Y)$
39	1 2 37 12 22 28 24 26 32 38	funcco	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to (z G Y) (R (⟨z, X⟩ comp (C) Y) f) = (X G Y) (R) (⟨F (z), F (X)⟩ comp (D) F (Y)) (z G X) (f)$
40	1 2 37 12 22 28 24 26 34 38	funcco	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to (z G Y) (R (⟨z, X⟩ comp (C) Y) g) = (X G Y) (R) (⟨F (z), F (X)⟩ comp (D) F (Y)) (z G X) (g)$
41	39 40	eqeq12d	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to ((z G Y) (R (⟨z, X⟩ comp (C) Y) f) = (z G Y) (R (⟨z, X⟩ comp (C) Y) g) \leftrightarrow (X G Y) (R) (⟨F (z), F (X)⟩ comp (D) F (Y)) (z G X) (f) = (X G Y) (R) (⟨F (z), F (X)⟩ comp (D) F (Y)) (z G X) (g))$
42	3	adantr	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to F (C Faith D) G$
43	19	simpld	$⊢ φ \to C \in Cat$
44	43	adantr	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to C \in Cat$
45	1 2 37 44 28 24 26 32 38	catcocl	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to R (⟨z, X⟩ comp (C) Y) f \in (z H Y)$
46	1 2 37 44 28 24 26 34 38	catcocl	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to R (⟨z, X⟩ comp (C) Y) g \in (z H Y)$
47	1 2 11 42 28 26 45 46	fthi	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to ((z G Y) (R (⟨z, X⟩ comp (C) Y) f) = (z G Y) (R (⟨z, X⟩ comp (C) Y) g) \leftrightarrow R (⟨z, X⟩ comp (C) Y) f = R (⟨z, X⟩ comp (C) Y) g)$
48	41 47	bitr3d	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to ((X G Y) (R) (⟨F (z), F (X)⟩ comp (D) F (Y)) (z G X) (f) = (X G Y) (R) (⟨F (z), F (X)⟩ comp (D) F (Y)) (z G X) (g) \leftrightarrow R (⟨z, X⟩ comp (C) Y) f = R (⟨z, X⟩ comp (C) Y) g)$
49	1 2 11 42 28 24 32 34	fthi	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to ((z G X) (f) = (z G X) (g) \leftrightarrow f = g)$
50	36 48 49	3bitr3d	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to (R (⟨z, X⟩ comp (C) Y) f = R (⟨z, X⟩ comp (C) Y) g \leftrightarrow f = g)$
51	50	biimpd	$⊢ (φ \land (z \in B \land f \in (z H X) \land g \in (z H X))) \to (R (⟨z, X⟩ comp (C) Y) f = R (⟨z, X⟩ comp (C) Y) g \to f = g)$
52	51	ralrimivvva	$⊢ φ \to \forall z \in B \forall f \in (z H X) \forall g \in (z H X) (R (⟨z, X⟩ comp (C) Y) f = R (⟨z, X⟩ comp (C) Y) g \to f = g)$
53	1 2 37 7 43 4 5	ismon2	$⊢ φ \to (R \in (X M Y) \leftrightarrow (R \in (X H Y) \land \forall z \in B \forall f \in (z H X) \forall g \in (z H X) (R (⟨z, X⟩ comp (C) Y) f = R (⟨z, X⟩ comp (C) Y) g \to f = g)))$
54	6 52 53	mpbir2and	$⊢ φ \to R \in (X M Y)$

Metamath Proof Explorer

Theorem fthmon

Proof