Step | Hyp | Ref
| Expression |
1 | | invfuc.u |
. 2
⊢ (𝜑 → 𝑈 ∈ (𝐹𝑁𝐺)) |
2 | | invfuc.v |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))𝑋) |
3 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝐷) =
(Base‘𝐷) |
4 | | fucinv.j |
. . . . . . . . . 10
⊢ 𝐽 = (Inv‘𝐷) |
5 | | fuciso.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
6 | | funcrcl 16346 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
8 | 7 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ Cat) |
9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ Cat) |
10 | | fuciso.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐶) |
11 | | relfunc 16345 |
. . . . . . . . . . . . 13
⊢ Rel
(𝐶 Func 𝐷) |
12 | | 1st2ndbr 7108 |
. . . . . . . . . . . . 13
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
13 | 11, 5, 12 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
14 | 10, 3, 13 | funcf1 16349 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘𝐹):𝐵⟶(Base‘𝐷)) |
15 | 14 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
16 | | fuciso.g |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
17 | | 1st2ndbr 7108 |
. . . . . . . . . . . . 13
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
18 | 11, 16, 17 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
19 | 10, 3, 18 | funcf1 16349 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘𝐺):𝐵⟶(Base‘𝐷)) |
20 | 19 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐷)) |
21 | | eqid 2610 |
. . . . . . . . . 10
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
22 | 3, 4, 9, 15, 20, 21 | invss 16244 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) ⊆ ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))) |
23 | 22 | ssbrd 4626 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))𝑋 → (𝑈‘𝑥)((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))𝑋)) |
24 | 2, 23 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))𝑋) |
25 | | brxp 5071 |
. . . . . . . 8
⊢ ((𝑈‘𝑥)((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))𝑋 ↔ ((𝑈‘𝑥) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) ∧ 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))) |
26 | 25 | simprbi 479 |
. . . . . . 7
⊢ ((𝑈‘𝑥)((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))𝑋 → 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) |
27 | 24, 26 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) |
28 | 27 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) |
29 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
30 | 10, 29 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
31 | | mptelixpg 7831 |
. . . . . 6
⊢ (𝐵 ∈ V → ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))) |
32 | 30, 31 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) |
33 | 28, 32 | sylibr 223 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) |
34 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((1st ‘𝐺)‘𝑥) = ((1st ‘𝐺)‘𝑦)) |
35 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((1st ‘𝐹)‘𝑥) = ((1st ‘𝐹)‘𝑦)) |
36 | 34, 35 | oveq12d 6567 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)) = (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
37 | 36 | cbvixpv 7812 |
. . . 4
⊢ X𝑥 ∈
𝐵 (((1st
‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)) = X𝑦 ∈ 𝐵 (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) |
38 | 33, 37 | syl6eleq 2698 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑦 ∈ 𝐵 (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
39 | | simpr2 1061 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ 𝐵) |
40 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
41 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐵 ↦ 𝑋) = (𝑥 ∈ 𝐵 ↦ 𝑋) |
42 | 41 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) |
43 | 40, 27, 42 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) |
44 | 2, 43 | breqtrrd 4611 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) |
45 | 44 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) |
47 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑈‘𝑧) |
48 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧)) |
49 | | nffvmpt1 6111 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) |
50 | 47, 48, 49 | nfbr 4629 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) |
51 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝑈‘𝑥) = (𝑈‘𝑧)) |
52 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → ((1st ‘𝐹)‘𝑥) = ((1st ‘𝐹)‘𝑧)) |
53 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → ((1st ‘𝐺)‘𝑥) = ((1st ‘𝐺)‘𝑧)) |
54 | 52, 53 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) = (((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))) |
55 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)) |
56 | 51, 54, 55 | breq123d 4597 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ((𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ (𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))) |
57 | 50, 56 | rspc 3276 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) → (𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))) |
58 | 39, 46, 57 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)) |
59 | 8 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐷 ∈ Cat) |
60 | 14 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹):𝐵⟶(Base‘𝐷)) |
61 | 60, 39 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷)) |
62 | 19 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺):𝐵⟶(Base‘𝐷)) |
63 | 62, 39 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑧) ∈ (Base‘𝐷)) |
64 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Sect‘𝐷) =
(Sect‘𝐷) |
65 | 3, 4, 59, 61, 63, 64 | isinv 16243 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ↔ ((𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)(Sect‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(((1st ‘𝐺)‘𝑧)(Sect‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧)))) |
66 | 58, 65 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)(Sect‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(((1st ‘𝐺)‘𝑧)(Sect‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧))) |
67 | 66 | simpld 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)(Sect‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)) |
68 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(comp‘𝐷) =
(comp‘𝐷) |
69 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Id‘𝐷) =
(Id‘𝐷) |
70 | 3, 21, 68, 69, 64, 59, 61, 63 | issect 16236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)(Sect‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ↔ ((𝑈‘𝑧) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)) ∧ (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑧))))) |
71 | 67, 70 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)) ∧ (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑧)))) |
72 | 71 | simp3d 1068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑧))) |
73 | 72 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) = (((Id‘𝐷)‘((1st ‘𝐹)‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓))) |
74 | | simpr1 1060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ 𝐵) |
75 | 60, 74 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) |
76 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
77 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
78 | 10, 76, 21, 77, 74, 39 | funcf2 16351 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) |
79 | | simpr3 1062 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)) |
80 | 78, 79 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑓) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) |
81 | 3, 21, 69, 59, 75, 68, 61, 80 | catlid 16167 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((Id‘𝐷)‘((1st ‘𝐹)‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) = ((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) |
82 | 73, 81 | eqtr2d 2645 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑓) = ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓))) |
83 | | fuciso.n |
. . . . . . . . 9
⊢ 𝑁 = (𝐶 Nat 𝐷) |
84 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (𝐹𝑁𝐺)) |
85 | 83, 84 | nat1st2nd 16434 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) |
86 | 83, 85, 10, 21, 39 | natcl 16436 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧))) |
87 | 71 | simp2d 1067 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) |
88 | 3, 21, 68, 59, 75, 61, 63, 80, 86, 61, 87 | catass 16170 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑈‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)))) |
89 | 83, 85, 10, 76, 68, 74, 39, 79 | nati 16438 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))) |
90 | 89 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑈‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓))) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)))) |
91 | 82, 88, 90 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑓) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)))) |
92 | 91 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐹)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) |
93 | 62, 74 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐷)) |
94 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑈‘𝑦) |
95 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦)) |
96 | | nffvmpt1 6111 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) |
97 | 94, 95, 96 | nfbr 4629 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) |
98 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑈‘𝑥) = (𝑈‘𝑦)) |
99 | 35, 34 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) = (((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))) |
100 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) |
101 | 98, 99, 100 | breq123d 4597 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) |
102 | 97, 101 | rspc 3276 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) → (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) |
103 | 74, 46, 102 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) |
104 | 3, 4, 59, 75, 93, 64 | isinv 16243 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ↔ ((𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)(Sect‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1st ‘𝐺)‘𝑦)(Sect‘𝐷)((1st ‘𝐹)‘𝑦))(𝑈‘𝑦)))) |
105 | 103, 104 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)(Sect‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1st ‘𝐺)‘𝑦)(Sect‘𝐷)((1st ‘𝐹)‘𝑦))(𝑈‘𝑦))) |
106 | 105 | simprd 478 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1st ‘𝐺)‘𝑦)(Sect‘𝐷)((1st ‘𝐹)‘𝑦))(𝑈‘𝑦)) |
107 | 3, 21, 68, 69, 64, 59, 93, 75 | issect 16236 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1st ‘𝐺)‘𝑦)(Sect‘𝐷)((1st ‘𝐹)‘𝑦))(𝑈‘𝑦) ↔ (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) ∧ (𝑈‘𝑦) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑦)) ∧ ((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st ‘𝐺)‘𝑦))))) |
108 | 106, 107 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) ∧ (𝑈‘𝑦) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑦)) ∧ ((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st ‘𝐺)‘𝑦)))) |
109 | 108 | simp1d 1066 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
110 | 108 | simp2d 1067 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑦))) |
111 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
112 | 10, 76, 21, 111, 74, 39 | funcf2 16351 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧))) |
113 | 112, 79 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐺)𝑧)‘𝑓) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧))) |
114 | 3, 21, 68, 59, 75, 93, 63, 110, 113 | catcocl 16169 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧))) |
115 | 3, 21, 68, 59, 93, 75, 63, 109, 114, 61, 87 | catass 16170 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))) |
116 | 83, 85, 10, 21, 74 | natcl 16436 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑦))) |
117 | 3, 21, 68, 59, 93, 75, 93, 109, 116, 63, 113 | catass 16170 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))) |
118 | 108 | simp3d 1068 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st ‘𝐺)‘𝑦))) |
119 | 118 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((Id‘𝐷)‘((1st ‘𝐺)‘𝑦)))) |
120 | 3, 21, 69, 59, 93, 68, 63, 113 | catrid 16168 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((Id‘𝐷)‘((1st ‘𝐺)‘𝑦))) = ((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) |
121 | 117, 119,
120 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) |
122 | 121 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐺)𝑧)‘𝑓))) |
123 | 92, 115, 122 | 3eqtrrd 2649 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) |
124 | 123 | ralrimivvva 2955 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) |
125 | 83, 10, 76, 21, 68, 16, 5 | isnat2 16431 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹) ↔ ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑦 ∈ 𝐵 (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))))) |
126 | 38, 124, 125 | mpbir2and 959 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹)) |
127 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑦(𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) |
128 | 127, 97, 101 | cbvral 3143 |
. . 3
⊢
(∀𝑥 ∈
𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) |
129 | 45, 128 | sylib 207 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) |
130 | | fuciso.q |
. . 3
⊢ 𝑄 = (𝐶 FuncCat 𝐷) |
131 | | fucinv.i |
. . 3
⊢ 𝐼 = (Inv‘𝑄) |
132 | 130, 10, 83, 5, 16, 131, 4 | fucinv 16456 |
. 2
⊢ (𝜑 → (𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋) ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹) ∧ ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))) |
133 | 1, 126, 129, 132 | mpbir3and 1238 |
1
⊢ (𝜑 → 𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋)) |