fthepi

Description: A faithful functor reflects epimorphisms. (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)$
	fthepi.e	$⊢ E = Epi (C)$
	fthepi.p	$⊢ P = Epi (D)$
	fthepi.1	$⊢ φ \to (X G Y) (R) \in (F (X) P F (Y))$
Assertion	fthepi	$⊢ φ \to R \in (X E 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		fthepi.e	$⊢ E = Epi (C)$
8		fthepi.p	$⊢ P = Epi (D)$
9		fthepi.1	$⊢ φ \to (X G Y) (R) \in (F (X) P F (Y))$
10		eqid	$⊢ oppCat (C) = oppCat (C)$
11	10 1	oppcbas	$⊢ B = {Base}_{oppCat (C)}$
12		eqid	$⊢ Hom (oppCat (C)) = Hom (oppCat (C))$
13		eqid	$⊢ oppCat (D) = oppCat (D)$
14	10 13 3	fthoppc	$⊢ φ \to F (oppCat (C) Faith oppCat (D)) tpos G$
15	2 10	oppchom	$⊢ Y Hom (oppCat (C)) X = X H Y$
16	6 15	eleqtrrdi	$⊢ φ \to R \in (Y Hom (oppCat (C)) X)$
17		eqid	$⊢ Mono (oppCat (C)) = Mono (oppCat (C))$
18		eqid	$⊢ Mono (oppCat (D)) = Mono (oppCat (D))$
19		ovtpos	$⊢ Y tpos G X = X G Y$
20	19	fveq1i	$⊢ (Y tpos G X) (R) = (X G Y) (R)$
21	20 9	eqeltrid	$⊢ φ \to (Y tpos G X) (R) \in (F (X) P F (Y))$
22		fthfunc	$⊢ C Faith D \subseteq C Func D$
23	22	ssbri	$⊢ F (C Faith D) G \to F (C Func D) G$
24	3 23	syl	$⊢ φ \to F (C Func D) G$
25		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
26	24 25	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
27		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
28	26 27	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
29	28	simprd	$⊢ φ \to D \in Cat$
30	13 29 18 8	oppcmon	$⊢ φ \to F (Y) Mono (oppCat (D)) F (X) = F (X) P F (Y)$
31	21 30	eleqtrrd	$⊢ φ \to (Y tpos G X) (R) \in (F (Y) Mono (oppCat (D)) F (X))$
32	11 12 14 5 4 16 17 18 31	fthmon	$⊢ φ \to R \in (Y Mono (oppCat (C)) X)$
33	28	simpld	$⊢ φ \to C \in Cat$
34	10 33 17 7	oppcmon	$⊢ φ \to Y Mono (oppCat (C)) X = X E Y$
35	32 34	eleqtrd	$⊢ φ \to R \in (X E Y)$

Metamath Proof Explorer

Theorem fthepi

Proof