Metamath Proof Explorer

Theorem 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 ⊢ φ → F C Faith D G
fthsect.x ⊢ φ → X ∈ B
fthsect.y ⊢ φ → Y ∈ B
fthsect.m ⊢ φ → M ∈ X H Y
fthsect.n ⊢ φ → N ∈ Y H X
fthsect.s ⊢ S = Sect ⁡ C
fthsect.t ⊢ T = Sect ⁡ D
Assertion fthsect ⊢ φ → M X S Y N ↔ 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 ⊢ φ → F C Faith D G
4 fthsect.x ⊢ φ → X ∈ B
5 fthsect.y ⊢ φ → Y ∈ B
6 fthsect.m ⊢ φ → M ∈ X H Y
7 fthsect.n ⊢ φ → N ∈ 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 ⊆ C Func D
13 12 ssbri ⊢ F C Faith D G → F C Func D G
14 3 13 syl ⊢ φ → F C Func D G
15 df-br ⊢ F C Func D G ↔ F G ∈ C Func D
16 14 15 sylib ⊢ φ → F G ∈ C Func D
17 funcrcl ⊢ F G ∈ C Func D → C ∈ Cat ∧ D ∈ Cat
18 16 17 syl ⊢ φ → C ∈ Cat ∧ D ∈ Cat
19 18 simpld ⊢ φ → C ∈ Cat
20 1 2 11 19 4 5 4 6 7 catcocl ⊢ φ → N X Y comp ⁡ C X M ∈ X H X
21 eqid ⊢ Id ⁡ C = Id ⁡ C
22 1 2 21 19 4 catidcl ⊢ φ → Id ⁡ C ⁡ X ∈ X H X
23 1 2 10 3 4 4 20 22 fthi ⊢ φ → X G X ⁡ N X Y comp ⁡ C X M = X G X ⁡ Id ⁡ C ⁡ X ↔ 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 ⊢ φ → 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 ⊢ φ → X G X ⁡ Id ⁡ C ⁡ X = Id ⁡ D ⁡ F ⁡ X
28 25 27 eqeq12d ⊢ φ → X G X ⁡ N X Y comp ⁡ C X M = X G X ⁡ Id ⁡ C ⁡ X ↔ Y G X ⁡ N F ⁡ X F ⁡ Y comp ⁡ D F ⁡ X X G Y ⁡ M = Id ⁡ D ⁡ F ⁡ X
29 23 28 bitr3d ⊢ φ → N X Y comp ⁡ C X M = Id ⁡ C ⁡ X ↔ 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 ⊢ φ → M X S Y N ↔ N X Y comp ⁡ C X M = Id ⁡ C ⁡ X
31 eqid ⊢ Base D = Base D
32 18 simprd ⊢ φ → D ∈ Cat
33 1 31 14 funcf1 ⊢ φ → F : B ⟶ Base D
34 33 4 ffvelcdmd ⊢ φ → F ⁡ X ∈ Base D
35 33 5 ffvelcdmd ⊢ φ → F ⁡ Y ∈ Base D
36 1 2 10 14 4 5 funcf2 ⊢ φ → X G Y : X H Y ⟶ F ⁡ X Hom ⁡ D F ⁡ Y
37 36 6 ffvelcdmd ⊢ φ → X G Y ⁡ M ∈ F ⁡ X Hom ⁡ D F ⁡ Y
38 1 2 10 14 5 4 funcf2 ⊢ φ → Y G X : Y H X ⟶ F ⁡ Y Hom ⁡ D F ⁡ X
39 38 7 ffvelcdmd ⊢ φ → Y G X ⁡ N ∈ F ⁡ Y Hom ⁡ D F ⁡ X
40 31 10 24 26 9 32 34 35 37 39 issect2 ⊢ φ → X G Y ⁡ M F ⁡ X T F ⁡ Y Y G X ⁡ N ↔ 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 ⊢ φ → M X S Y N ↔ X G Y ⁡ M F ⁡ X T F ⁡ Y Y G X ⁡ N