Proof of Theorem cvmlift3lem6
Step | Hyp | Ref
| Expression |
1 | | cvmlift3lem6.q |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (II Cn 𝐾)) |
2 | | cvmlift3.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ SConn) |
3 | | sconntop 32763 |
. . . . . . . 8
⊢ (𝐾 ∈ SConn → 𝐾 ∈ Top) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
5 | | cnrest2r 22040 |
. . . . . . 7
⊢ (𝐾 ∈ Top → (II Cn (𝐾 ↾t 𝑀)) ⊆ (II Cn 𝐾)) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → (II Cn (𝐾 ↾t 𝑀)) ⊆ (II Cn 𝐾)) |
7 | | cvmlift3lem6.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (II Cn (𝐾 ↾t 𝑀))) |
8 | 6, 7 | sseldd 3878 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (II Cn 𝐾)) |
9 | | cvmlift3lem6.1 |
. . . . . . 7
⊢ (𝜑 → ((𝑄‘0) = 𝑂 ∧ (𝑄‘1) = 𝑋 ∧ (𝑅‘1) = (𝐻‘𝑋))) |
10 | 9 | simp2d 1144 |
. . . . . 6
⊢ (𝜑 → (𝑄‘1) = 𝑋) |
11 | | cvmlift3lem6.2 |
. . . . . . 7
⊢ (𝜑 → ((𝑁‘0) = 𝑋 ∧ (𝑁‘1) = 𝑍)) |
12 | 11 | simpld 498 |
. . . . . 6
⊢ (𝜑 → (𝑁‘0) = 𝑋) |
13 | 10, 12 | eqtr4d 2776 |
. . . . 5
⊢ (𝜑 → (𝑄‘1) = (𝑁‘0)) |
14 | 1, 8, 13 | pcocn 23771 |
. . . 4
⊢ (𝜑 → (𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾)) |
15 | 1, 8 | pco0 23768 |
. . . . 5
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘0) = (𝑄‘0)) |
16 | 9 | simp1d 1143 |
. . . . 5
⊢ (𝜑 → (𝑄‘0) = 𝑂) |
17 | 15, 16 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂) |
18 | 1, 8 | pco1 23769 |
. . . . 5
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘1) = (𝑁‘1)) |
19 | 11 | simprd 499 |
. . . . 5
⊢ (𝜑 → (𝑁‘1) = 𝑍) |
20 | 18, 19 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍) |
21 | | cvmlift3.b |
. . . . . . . . . . 11
⊢ 𝐵 = ∪
𝐶 |
22 | | cvmlift3lem6.r |
. . . . . . . . . . 11
⊢ 𝑅 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑄) ∧ (𝑔‘0) = 𝑃)) |
23 | | cvmlift3.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
24 | | cvmlift3.g |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) |
25 | | cnco 22019 |
. . . . . . . . . . . 12
⊢ ((𝑄 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑄) ∈ (II Cn 𝐽)) |
26 | 1, 24, 25 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∘ 𝑄) ∈ (II Cn 𝐽)) |
27 | | cvmlift3.p |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
28 | 16 | fveq2d 6680 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘(𝑄‘0)) = (𝐺‘𝑂)) |
29 | | iiuni 23635 |
. . . . . . . . . . . . . . 15
⊢ (0[,]1) =
∪ II |
30 | | cvmlift3.y |
. . . . . . . . . . . . . . 15
⊢ 𝑌 = ∪
𝐾 |
31 | 29, 30 | cnf 21999 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (II Cn 𝐾) → 𝑄:(0[,]1)⟶𝑌) |
32 | 1, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄:(0[,]1)⟶𝑌) |
33 | | 0elunit 12945 |
. . . . . . . . . . . . 13
⊢ 0 ∈
(0[,]1) |
34 | | fvco3 6769 |
. . . . . . . . . . . . 13
⊢ ((𝑄:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) →
((𝐺 ∘ 𝑄)‘0) = (𝐺‘(𝑄‘0))) |
35 | 32, 33, 34 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝑄)‘0) = (𝐺‘(𝑄‘0))) |
36 | | cvmlift3.e |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) |
37 | 28, 35, 36 | 3eqtr4rd 2784 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ 𝑄)‘0)) |
38 | 21, 22, 23, 26, 27, 37 | cvmliftiota 32836 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝑅) = (𝐺 ∘ 𝑄) ∧ (𝑅‘0) = 𝑃)) |
39 | 38 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘ 𝑅) = (𝐺 ∘ 𝑄)) |
40 | | cvmlift3lem6.i |
. . . . . . . . . . 11
⊢ 𝐼 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑁) ∧ (𝑔‘0) = (𝐻‘𝑋))) |
41 | | cnco 22019 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑁) ∈ (II Cn 𝐽)) |
42 | 8, 24, 41 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∘ 𝑁) ∈ (II Cn 𝐽)) |
43 | | cvmlift3.l |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
PConn) |
44 | | cvmlift3.o |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑂 ∈ 𝑌) |
45 | | cvmlift3.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) |
46 | 21, 30, 23, 2, 43, 44, 24, 27, 36, 45 | cvmlift3lem3 32856 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻:𝑌⟶𝐵) |
47 | | cvmlift3lem7.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ⊆ (◡𝐺 “ 𝐴)) |
48 | | cnvimass 5923 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐺 “ 𝐴) ⊆ dom 𝐺 |
49 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝐽 =
∪ 𝐽 |
50 | 30, 49 | cnf 21999 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽) |
51 | 24, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽) |
52 | 48, 51 | fssdm 6524 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝐺 “ 𝐴) ⊆ 𝑌) |
53 | 47, 52 | sstrd 3887 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ⊆ 𝑌) |
54 | | cvmlift3lem6.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝑀) |
55 | 53, 54 | sseldd 3878 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑌) |
56 | 46, 55 | ffvelrnd 6864 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝐵) |
57 | 12 | fveq2d 6680 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘(𝑁‘0)) = (𝐺‘𝑋)) |
58 | 29, 30 | cnf 21999 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (II Cn 𝐾) → 𝑁:(0[,]1)⟶𝑌) |
59 | 8, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁:(0[,]1)⟶𝑌) |
60 | | fvco3 6769 |
. . . . . . . . . . . . 13
⊢ ((𝑁:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) →
((𝐺 ∘ 𝑁)‘0) = (𝐺‘(𝑁‘0))) |
61 | 59, 33, 60 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ∘ 𝑁)‘0) = (𝐺‘(𝑁‘0))) |
62 | | fvco3 6769 |
. . . . . . . . . . . . . 14
⊢ ((𝐻:𝑌⟶𝐵 ∧ 𝑋 ∈ 𝑌) → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋))) |
63 | 46, 55, 62 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋))) |
64 | 21, 30, 23, 2, 43, 44, 24, 27, 36, 45 | cvmlift3lem5 32858 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) |
65 | 64 | fveq1d 6678 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐺‘𝑋)) |
66 | 63, 65 | eqtr3d 2775 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = (𝐺‘𝑋)) |
67 | 57, 61, 66 | 3eqtr4rd 2784 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = ((𝐺 ∘ 𝑁)‘0)) |
68 | 21, 40, 23, 42, 56, 67 | cvmliftiota 32836 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐼) = (𝐺 ∘ 𝑁) ∧ (𝐼‘0) = (𝐻‘𝑋))) |
69 | 68 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘ 𝐼) = (𝐺 ∘ 𝑁)) |
70 | 39, 69 | oveq12d 7190 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ∘ 𝑅)(*𝑝‘𝐽)(𝐹 ∘ 𝐼)) = ((𝐺 ∘ 𝑄)(*𝑝‘𝐽)(𝐺 ∘ 𝑁))) |
71 | 38 | simp1d 1143 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (II Cn 𝐶)) |
72 | 68 | simp1d 1143 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐶)) |
73 | 9 | simp3d 1145 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅‘1) = (𝐻‘𝑋)) |
74 | 68 | simp3d 1145 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼‘0) = (𝐻‘𝑋)) |
75 | 73, 74 | eqtr4d 2776 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅‘1) = (𝐼‘0)) |
76 | | cvmcn 32797 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
77 | 23, 76 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽)) |
78 | 71, 72, 75, 77 | copco 23772 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = ((𝐹 ∘ 𝑅)(*𝑝‘𝐽)(𝐹 ∘ 𝐼))) |
79 | 1, 8, 13, 24 | copco 23772 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) = ((𝐺 ∘ 𝑄)(*𝑝‘𝐽)(𝐺 ∘ 𝑁))) |
80 | 70, 78, 79 | 3eqtr4d 2783 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))) |
81 | 71, 72 | pco0 23768 |
. . . . . . . 8
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘0) = (𝑅‘0)) |
82 | 38 | simp3d 1145 |
. . . . . . . 8
⊢ (𝜑 → (𝑅‘0) = 𝑃) |
83 | 81, 82 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) |
84 | 71, 72, 75 | pcocn 23771 |
. . . . . . . 8
⊢ (𝜑 → (𝑅(*𝑝‘𝐶)𝐼) ∈ (II Cn 𝐶)) |
85 | | cnco 22019 |
. . . . . . . . . 10
⊢ (((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) |
86 | 14, 24, 85 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) |
87 | 17 | fveq2d 6680 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0)) = (𝐺‘𝑂)) |
88 | 29, 30 | cnf 21999 |
. . . . . . . . . . . 12
⊢ ((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) → (𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌) |
89 | 14, 88 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌) |
90 | | fvco3 6769 |
. . . . . . . . . . 11
⊢ (((𝑄(*𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0) = (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0))) |
91 | 89, 33, 90 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0) = (𝐺‘((𝑄(*𝑝‘𝐾)𝑁)‘0))) |
92 | 87, 91, 36 | 3eqtr4rd 2784 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0)) |
93 | 21 | cvmlift 32834 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = ((𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) |
94 | 23, 86, 27, 92, 93 | syl22anc 838 |
. . . . . . . 8
⊢ (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) |
95 | | coeq2 5701 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼))) |
96 | 95 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ↔ (𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)))) |
97 | | fveq1 6675 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (𝑔‘0) = ((𝑅(*𝑝‘𝐶)𝐼)‘0)) |
98 | 97 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → ((𝑔‘0) = 𝑃 ↔ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃)) |
99 | 96, 98 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑔 = (𝑅(*𝑝‘𝐶)𝐼) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃))) |
100 | 99 | riota2 7155 |
. . . . . . . 8
⊢ (((𝑅(*𝑝‘𝐶)𝐼) ∈ (II Cn 𝐶) ∧ ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) → (((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼))) |
101 | 84, 94, 100 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (((𝐹 ∘ (𝑅(*𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ ((𝑅(*𝑝‘𝐶)𝐼)‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼))) |
102 | 80, 83, 101 | mpbi2and 712 |
. . . . . 6
⊢ (𝜑 → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*𝑝‘𝐶)𝐼)) |
103 | 102 | fveq1d 6678 |
. . . . 5
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = ((𝑅(*𝑝‘𝐶)𝐼)‘1)) |
104 | 71, 72 | pco1 23769 |
. . . . 5
⊢ (𝜑 → ((𝑅(*𝑝‘𝐶)𝐼)‘1) = (𝐼‘1)) |
105 | 103, 104 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)) |
106 | | fveq1 6675 |
. . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝑓‘0) = ((𝑄(*𝑝‘𝐾)𝑁)‘0)) |
107 | 106 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝑓‘0) = 𝑂 ↔ ((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂)) |
108 | | fveq1 6675 |
. . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝑓‘1) = ((𝑄(*𝑝‘𝐾)𝑁)‘1)) |
109 | 108 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝑓‘1) = 𝑍 ↔ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍)) |
110 | | coeq2 5701 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (𝐺 ∘ 𝑓) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁))) |
111 | 110 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)))) |
112 | 111 | anbi1d 633 |
. . . . . . . . 9
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))) |
113 | 112 | riotabidv 7131 |
. . . . . . . 8
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))) |
114 | 113 | fveq1d 6678 |
. . . . . . 7
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1)) |
115 | 114 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1) ↔ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) |
116 | 107, 109,
115 | 3anbi123d 1437 |
. . . . 5
⊢ (𝑓 = (𝑄(*𝑝‘𝐾)𝑁) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)) ↔ (((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) |
117 | 116 | rspcev 3526 |
. . . 4
⊢ (((𝑄(*𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) ∧ (((𝑄(*𝑝‘𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(*𝑝‘𝐾)𝑁)‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) |
118 | 14, 17, 20, 105, 117 | syl13anc 1373 |
. . 3
⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) |
119 | | cvmlift3lem6.z |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑀) |
120 | 53, 119 | sseldd 3878 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑌) |
121 | 21, 30, 23, 2, 43, 44, 24, 27, 36, 45 | cvmlift3lem4 32857 |
. . . 4
⊢ ((𝜑 ∧ 𝑍 ∈ 𝑌) → ((𝐻‘𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) |
122 | 120, 121 | mpdan 687 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))) |
123 | 118, 122 | mpbird 260 |
. 2
⊢ (𝜑 → (𝐻‘𝑍) = (𝐼‘1)) |
124 | | iiconn 23641 |
. . . . 5
⊢ II ∈
Conn |
125 | 124 | a1i 11 |
. . . 4
⊢ (𝜑 → II ∈
Conn) |
126 | | cvmtop1 32795 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
127 | 23, 126 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Top) |
128 | 21 | toptopon 21670 |
. . . . . . 7
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
129 | 127, 128 | sylib 221 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
130 | 69 | rneqd 5781 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝐹 ∘ 𝐼) = ran (𝐺 ∘ 𝑁)) |
131 | | rnco2 6086 |
. . . . . . . . 9
⊢ ran
(𝐹 ∘ 𝐼) = (𝐹 “ ran 𝐼) |
132 | | rnco2 6086 |
. . . . . . . . 9
⊢ ran
(𝐺 ∘ 𝑁) = (𝐺 “ ran 𝑁) |
133 | 130, 131,
132 | 3eqtr3g 2796 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ ran 𝐼) = (𝐺 “ ran 𝑁)) |
134 | | iitopon 23633 |
. . . . . . . . . . . . 13
⊢ II ∈
(TopOn‘(0[,]1)) |
135 | 134 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
136 | 30 | toptopon 21670 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
137 | 4, 136 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
138 | | resttopon 21914 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑀 ⊆ 𝑌) → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) |
139 | 137, 53, 138 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀)) |
140 | | cnf2 22002 |
. . . . . . . . . . . 12
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ (𝐾 ↾t 𝑀) ∈ (TopOn‘𝑀) ∧ 𝑁 ∈ (II Cn (𝐾 ↾t 𝑀))) → 𝑁:(0[,]1)⟶𝑀) |
141 | 135, 139,
7, 140 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁:(0[,]1)⟶𝑀) |
142 | 141 | frnd 6512 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑁 ⊆ 𝑀) |
143 | 142, 47 | sstrd 3887 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝑁 ⊆ (◡𝐺 “ 𝐴)) |
144 | 51 | ffund 6508 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐺) |
145 | 143, 48 | sstrdi 3889 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑁 ⊆ dom 𝐺) |
146 | | funimass3 6833 |
. . . . . . . . . 10
⊢ ((Fun
𝐺 ∧ ran 𝑁 ⊆ dom 𝐺) → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (◡𝐺 “ 𝐴))) |
147 | 144, 145,
146 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (◡𝐺 “ 𝐴))) |
148 | 143, 147 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 “ ran 𝑁) ⊆ 𝐴) |
149 | 133, 148 | eqsstrd 3915 |
. . . . . . 7
⊢ (𝜑 → (𝐹 “ ran 𝐼) ⊆ 𝐴) |
150 | 21, 49 | cnf 21999 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
151 | 77, 150 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽) |
152 | 151 | ffund 6508 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
153 | 29, 21 | cnf 21999 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (II Cn 𝐶) → 𝐼:(0[,]1)⟶𝐵) |
154 | 72, 153 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼:(0[,]1)⟶𝐵) |
155 | 154 | frnd 6512 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐼 ⊆ 𝐵) |
156 | 151 | fdmd 6515 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐵) |
157 | 155, 156 | sseqtrrd 3918 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐼 ⊆ dom 𝐹) |
158 | | funimass3 6833 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐼 ⊆ dom 𝐹) → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (◡𝐹 “ 𝐴))) |
159 | 152, 157,
158 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (◡𝐹 “ 𝐴))) |
160 | 149, 159 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → ran 𝐼 ⊆ (◡𝐹 “ 𝐴)) |
161 | | cnvimass 5923 |
. . . . . . 7
⊢ (◡𝐹 “ 𝐴) ⊆ dom 𝐹 |
162 | 161, 151 | fssdm 6524 |
. . . . . 6
⊢ (𝜑 → (◡𝐹 “ 𝐴) ⊆ 𝐵) |
163 | | cnrest2 22039 |
. . . . . 6
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran 𝐼 ⊆ (◡𝐹 “ 𝐴) ∧ (◡𝐹 “ 𝐴) ⊆ 𝐵) → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴))))) |
164 | 129, 160,
162, 163 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴))))) |
165 | 72, 164 | mpbid 235 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ (II Cn (𝐶 ↾t (◡𝐹 “ 𝐴)))) |
166 | | cvmlift3lem7.2 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴)) |
167 | | cvmlift3lem7.s |
. . . . . . . 8
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
168 | 167 | cvmsss 32802 |
. . . . . . 7
⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝑇 ⊆ 𝐶) |
169 | 166, 168 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑇 ⊆ 𝐶) |
170 | | cvmlift3lem7.1 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴) |
171 | 66, 170 | eqeltrd 2833 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) ∈ 𝐴) |
172 | | cvmlift3lem7.w |
. . . . . . . . 9
⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝐻‘𝑋) ∈ 𝑏) |
173 | 167, 21, 172 | cvmsiota 32812 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝐴) ∧ (𝐻‘𝑋) ∈ 𝐵 ∧ (𝐹‘(𝐻‘𝑋)) ∈ 𝐴)) → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) |
174 | 23, 166, 56, 171, 173 | syl13anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) |
175 | 174 | simpld 498 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝑇) |
176 | 169, 175 | sseldd 3878 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝐶) |
177 | | elssuni 4828 |
. . . . . . 7
⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇) |
178 | 175, 177 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇) |
179 | 167 | cvmsuni 32804 |
. . . . . . 7
⊢ (𝑇 ∈ (𝑆‘𝐴) → ∪ 𝑇 = (◡𝐹 “ 𝐴)) |
180 | 166, 179 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑇 =
(◡𝐹 “ 𝐴)) |
181 | 178, 180 | sseqtrd 3917 |
. . . . 5
⊢ (𝜑 → 𝑊 ⊆ (◡𝐹 “ 𝐴)) |
182 | 167 | cvmsrcl 32799 |
. . . . . . . 8
⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝐴 ∈ 𝐽) |
183 | 166, 182 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝐽) |
184 | | cnima 22018 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ 𝐶) |
185 | 77, 183, 184 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (◡𝐹 “ 𝐴) ∈ 𝐶) |
186 | | restopn2 21930 |
. . . . . 6
⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝐴) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (◡𝐹 “ 𝐴)))) |
187 | 127, 185,
186 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (◡𝐹 “ 𝐴)))) |
188 | 176, 181,
187 | mpbir2and 713 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝐴))) |
189 | 167 | cvmscld 32808 |
. . . . 5
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝐴) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝐴)))) |
190 | 23, 166, 175, 189 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝐴)))) |
191 | 33 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
(0[,]1)) |
192 | 174 | simprd 499 |
. . . . 5
⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝑊) |
193 | 74, 192 | eqeltrd 2833 |
. . . 4
⊢ (𝜑 → (𝐼‘0) ∈ 𝑊) |
194 | 29, 125, 165, 188, 190, 191, 193 | conncn 22179 |
. . 3
⊢ (𝜑 → 𝐼:(0[,]1)⟶𝑊) |
195 | | 1elunit 12946 |
. . 3
⊢ 1 ∈
(0[,]1) |
196 | | ffvelrn 6861 |
. . 3
⊢ ((𝐼:(0[,]1)⟶𝑊 ∧ 1 ∈ (0[,]1)) →
(𝐼‘1) ∈ 𝑊) |
197 | 194, 195,
196 | sylancl 589 |
. 2
⊢ (𝜑 → (𝐼‘1) ∈ 𝑊) |
198 | 123, 197 | eqeltrd 2833 |
1
⊢ (𝜑 → (𝐻‘𝑍) ∈ 𝑊) |