fthsect

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

	Ref	Expression
Hypotheses	fthsect.b	$⊢ B = {Base}_{C}$
	fthsect.h	$⊢ H = Hom (C)$
	fthsect.f	$⊢ φ \to F (C Faith D) G$
	fthsect.x	$⊢ φ \to X \in B$
	fthsect.y	$⊢ φ \to Y \in B$
	fthsect.m	$⊢ φ \to M \in (X H Y)$
	fthsect.n	$⊢ φ \to N \in (Y H X)$
	fthsect.s	$⊢ S = Sect (C)$
	fthsect.t	$⊢ T = Sect (D)$
Assertion	fthsect	$⊢ φ \to (M (X S Y) N \leftrightarrow (X G Y) (M) (F (X) T F (Y)) (Y G X) (N))$

Proof

Step	Hyp	Ref	Expression
1		fthsect.b	$⊢ B = {Base}_{C}$
2		fthsect.h	$⊢ H = Hom (C)$
3		fthsect.f	$⊢ φ \to F (C Faith D) G$
4		fthsect.x	$⊢ φ \to X \in B$
5		fthsect.y	$⊢ φ \to Y \in B$
6		fthsect.m	$⊢ φ \to M \in (X H Y)$
7		fthsect.n	$⊢ φ \to N \in (Y H X)$
8		fthsect.s	$⊢ S = Sect (C)$
9		fthsect.t	$⊢ T = Sect (D)$
10		eqid	$⊢ Hom (D) = Hom (D)$
11		eqid	$⊢ comp (C) = comp (C)$
12		fthfunc	$⊢ C Faith D \subseteq C Func D$
13	12	ssbri	$⊢ F (C Faith D) G \to F (C Func D) G$
14	3 13	syl	$⊢ φ \to F (C Func D) G$
15		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
16	14 15	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
17		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
18	16 17	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
19	18	simpld	$⊢ φ \to C \in Cat$
20	1 2 11 19 4 5 4 6 7	catcocl	$⊢ φ \to N (⟨X, Y⟩ comp (C) X) M \in (X H X)$
21		eqid	$⊢ Id (C) = Id (C)$
22	1 2 21 19 4	catidcl	$⊢ φ \to Id (C) (X) \in (X H X)$
23	1 2 10 3 4 4 20 22	fthi	$⊢ φ \to ((X G X) (N (⟨X, Y⟩ comp (C) X) M) = (X G X) (Id (C) (X)) \leftrightarrow N (⟨X, Y⟩ comp (C) X) M = Id (C) (X))$
24		eqid	$⊢ comp (D) = comp (D)$
25	1 2 11 24 14 4 5 4 6 7	funcco	$⊢ φ \to (X G X) (N (⟨X, Y⟩ comp (C) X) M) = (Y G X) (N) (⟨F (X), F (Y)⟩ comp (D) F (X)) (X G Y) (M)$
26		eqid	$⊢ Id (D) = Id (D)$
27	1 21 26 14 4	funcid	$⊢ φ \to (X G X) (Id (C) (X)) = Id (D) (F (X))$
28	25 27	eqeq12d	$⊢ φ \to ((X G X) (N (⟨X, Y⟩ comp (C) X) M) = (X G X) (Id (C) (X)) \leftrightarrow (Y G X) (N) (⟨F (X), F (Y)⟩ comp (D) F (X)) (X G Y) (M) = Id (D) (F (X)))$
29	23 28	bitr3d	$⊢ φ \to (N (⟨X, Y⟩ comp (C) X) M = Id (C) (X) \leftrightarrow (Y G X) (N) (⟨F (X), F (Y)⟩ comp (D) F (X)) (X G Y) (M) = Id (D) (F (X)))$
30	1 2 11 21 8 19 4 5 6 7	issect2	$⊢ φ \to (M (X S Y) N \leftrightarrow N (⟨X, Y⟩ comp (C) X) M = Id (C) (X))$
31		eqid	$⊢ {Base}_{D} = {Base}_{D}$
32	18	simprd	$⊢ φ \to D \in Cat$
33	1 31 14	funcf1	$⊢ φ \to F : B ⟶ {Base}_{D}$
34	33 4	ffvelcdmd	$⊢ φ \to F (X) \in {Base}_{D}$
35	33 5	ffvelcdmd	$⊢ φ \to F (Y) \in {Base}_{D}$
36	1 2 10 14 4 5	funcf2	$⊢ φ \to (X G Y) : X H Y ⟶ F (X) Hom (D) F (Y)$
37	36 6	ffvelcdmd	$⊢ φ \to (X G Y) (M) \in (F (X) Hom (D) F (Y))$
38	1 2 10 14 5 4	funcf2	$⊢ φ \to (Y G X) : Y H X ⟶ F (Y) Hom (D) F (X)$
39	38 7	ffvelcdmd	$⊢ φ \to (Y G X) (N) \in (F (Y) Hom (D) F (X))$
40	31 10 24 26 9 32 34 35 37 39	issect2	$⊢ φ \to ((X G Y) (M) (F (X) T F (Y)) (Y G X) (N) \leftrightarrow (Y G X) (N) (⟨F (X), F (Y)⟩ comp (D) F (X)) (X G Y) (M) = Id (D) (F (X)))$
41	29 30 40	3bitr4d	$⊢ φ \to (M (X S Y) N \leftrightarrow (X G Y) (M) (F (X) T F (Y)) (Y G X) (N))$

Metamath Proof Explorer

Theorem fthsect

Proof