Metamath Proof Explorer

Theorem fucsect

Description: Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses fuciso.q ⊢ Q = C FuncCat D
fuciso.b ⊢ B = Base C
fuciso.n ⊢ N = C Nat D
fuciso.f ⊢ φ → F ∈ C Func D
fuciso.g ⊢ φ → G ∈ C Func D
fucsect.s ⊢ S = Sect ⁡ Q
fucsect.t ⊢ T = Sect ⁡ D
Assertion fucsect ⊢ φ → U F S G V ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x

Proof

Step Hyp Ref Expression
1 fuciso.q ⊢ Q = C FuncCat D
2 fuciso.b ⊢ B = Base C
3 fuciso.n ⊢ N = C Nat D
4 fuciso.f ⊢ φ → F ∈ C Func D
5 fuciso.g ⊢ φ → G ∈ C Func D
6 fucsect.s ⊢ S = Sect ⁡ Q
7 fucsect.t ⊢ T = Sect ⁡ D
8 1 fucbas ⊢ C Func D = Base Q
9 1 3 fuchom ⊢ N = Hom ⁡ Q
10 eqid ⊢ comp ⁡ Q = comp ⁡ Q
11 eqid ⊢ Id ⁡ Q = Id ⁡ Q
12 funcrcl ⊢ F ∈ C Func D → C ∈ Cat ∧ D ∈ Cat
13 4 12 syl ⊢ φ → C ∈ Cat ∧ D ∈ Cat
14 13 simpld ⊢ φ → C ∈ Cat
15 13 simprd ⊢ φ → D ∈ Cat
16 1 14 15 fuccat ⊢ φ → Q ∈ Cat
17 8 9 10 11 6 16 4 5 issect ⊢ φ → U F S G V ↔ U ∈ F N G ∧ V ∈ G N F ∧ V F G comp ⁡ Q F U = Id ⁡ Q ⁡ F
18 ovex ⊢ V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ∈ V
19 18 rgenw ⊢ ∀ x ∈ B V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ∈ V
20 mpteqb ⊢ ∀ x ∈ B V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ∈ V → x ∈ B ⟼ V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x = x ∈ B ⟼ Id ⁡ D ⁡ 1 st ⁡ F ⁡ x ↔ ∀ x ∈ B V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x = Id ⁡ D ⁡ 1 st ⁡ F ⁡ x
21 19 20 mp1i ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → x ∈ B ⟼ V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x = x ∈ B ⟼ Id ⁡ D ⁡ 1 st ⁡ F ⁡ x ↔ ∀ x ∈ B V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x = Id ⁡ D ⁡ 1 st ⁡ F ⁡ x
22 eqid ⊢ comp ⁡ D = comp ⁡ D
23 simprl ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → U ∈ F N G
24 simprr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → V ∈ G N F
25 1 3 2 22 10 23 24 fucco ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → V F G comp ⁡ Q F U = x ∈ B ⟼ V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
26 eqid ⊢ Id ⁡ D = Id ⁡ D
27 4 adantr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → F ∈ C Func D
28 1 11 26 27 fucid ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → Id ⁡ Q ⁡ F = Id ⁡ D ∘ 1 st ⁡ F
29 15 adantr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → D ∈ Cat
30 eqid ⊢ Base D = Base D
31 30 26 cidfn ⊢ D ∈ Cat → Id ⁡ D Fn Base D
32 29 31 syl ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → Id ⁡ D Fn Base D
33 dffn2 ⊢ Id ⁡ D Fn Base D ↔ Id ⁡ D : Base D ⟶ V
34 32 33 sylib ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → Id ⁡ D : Base D ⟶ V
35 relfunc ⊢ Rel ⁡ C Func D
36 1st2ndbr ⊢ Rel ⁡ C Func D ∧ F ∈ C Func D → 1 st ⁡ F C Func D 2 nd ⁡ F
37 35 4 36 sylancr ⊢ φ → 1 st ⁡ F C Func D 2 nd ⁡ F
38 2 30 37 funcf1 ⊢ φ → 1 st ⁡ F : B ⟶ Base D
39 38 adantr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → 1 st ⁡ F : B ⟶ Base D
40 fcompt ⊢ Id ⁡ D : Base D ⟶ V ∧ 1 st ⁡ F : B ⟶ Base D → Id ⁡ D ∘ 1 st ⁡ F = x ∈ B ⟼ Id ⁡ D ⁡ 1 st ⁡ F ⁡ x
41 34 39 40 syl2anc ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → Id ⁡ D ∘ 1 st ⁡ F = x ∈ B ⟼ Id ⁡ D ⁡ 1 st ⁡ F ⁡ x
42 28 41 eqtrd ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → Id ⁡ Q ⁡ F = x ∈ B ⟼ Id ⁡ D ⁡ 1 st ⁡ F ⁡ x
43 25 42 eqeq12d ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → V F G comp ⁡ Q F U = Id ⁡ Q ⁡ F ↔ x ∈ B ⟼ V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x = x ∈ B ⟼ Id ⁡ D ⁡ 1 st ⁡ F ⁡ x
44 eqid ⊢ Hom ⁡ D = Hom ⁡ D
45 29 adantr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → D ∈ Cat
46 39 ffvelrnda ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → 1 st ⁡ F ⁡ x ∈ Base D
47 1st2ndbr ⊢ Rel ⁡ C Func D ∧ G ∈ C Func D → 1 st ⁡ G C Func D 2 nd ⁡ G
48 35 5 47 sylancr ⊢ φ → 1 st ⁡ G C Func D 2 nd ⁡ G
49 2 30 48 funcf1 ⊢ φ → 1 st ⁡ G : B ⟶ Base D
50 49 adantr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → 1 st ⁡ G : B ⟶ Base D
51 50 ffvelrnda ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → 1 st ⁡ G ⁡ x ∈ Base D
52 23 adantr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → U ∈ F N G
53 3 52 nat1st2nd ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → U ∈ 1 st ⁡ F 2 nd ⁡ F N 1 st ⁡ G 2 nd ⁡ G
54 simpr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → x ∈ B
55 3 53 2 44 54 natcl ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → U ⁡ x ∈ 1 st ⁡ F ⁡ x Hom ⁡ D 1 st ⁡ G ⁡ x
56 24 adantr ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → V ∈ G N F
57 3 56 nat1st2nd ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → V ∈ 1 st ⁡ G 2 nd ⁡ G N 1 st ⁡ F 2 nd ⁡ F
58 3 57 2 44 54 natcl ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → V ⁡ x ∈ 1 st ⁡ G ⁡ x Hom ⁡ D 1 st ⁡ F ⁡ x
59 30 44 22 26 7 45 46 51 55 58 issect2 ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F ∧ x ∈ B → U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x ↔ V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x = Id ⁡ D ⁡ 1 st ⁡ F ⁡ x
60 59 ralbidva ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x ↔ ∀ x ∈ B V ⁡ x 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x comp ⁡ D 1 st ⁡ F ⁡ x U ⁡ x = Id ⁡ D ⁡ 1 st ⁡ F ⁡ x
61 21 43 60 3bitr4d ⊢ φ ∧ U ∈ F N G ∧ V ∈ G N F → V F G comp ⁡ Q F U = Id ⁡ Q ⁡ F ↔ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x
62 61 pm5.32da ⊢ φ → U ∈ F N G ∧ V ∈ G N F ∧ V F G comp ⁡ Q F U = Id ⁡ Q ⁡ F ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x
63 df-3an ⊢ U ∈ F N G ∧ V ∈ G N F ∧ V F G comp ⁡ Q F U = Id ⁡ Q ⁡ F ↔ U ∈ F N G ∧ V ∈ G N F ∧ V F G comp ⁡ Q F U = Id ⁡ Q ⁡ F
64 df-3an ⊢ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x
65 62 63 64 3bitr4g ⊢ φ → U ∈ F N G ∧ V ∈ G N F ∧ V F G comp ⁡ Q F U = Id ⁡ Q ⁡ F ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x
66 17 65 bitrd ⊢ φ → U F S G V ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x T 1 st ⁡ G ⁡ x V ⁡ x