Proof of Theorem cvmliftlem8
Step | Hyp | Ref
| Expression |
1 | | elfznn 12241 |
. . 3
⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℕ) |
2 | | cvmliftlem.1 |
. . . 4
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) |
3 | | cvmliftlem.b |
. . . 4
⊢ 𝐵 = ∪
𝐶 |
4 | | cvmliftlem.x |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
5 | | cvmliftlem.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
6 | | cvmliftlem.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
7 | | cvmliftlem.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
8 | | cvmliftlem.e |
. . . 4
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) |
9 | | cvmliftlem.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
10 | | cvmliftlem.t |
. . . 4
⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪
𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) |
11 | | cvmliftlem.a |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) |
12 | | cvmliftlem.l |
. . . 4
⊢ 𝐿 = (topGen‘ran
(,)) |
13 | | cvmliftlem.q |
. . . 4
⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})) |
14 | | cvmliftlem5.3 |
. . . 4
⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) |
15 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | cvmliftlem5 30525 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑄‘𝑀) = (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) |
16 | 1, 15 | sylan2 490 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑄‘𝑀) = (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) |
17 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
18 | | cvmtop1 30496 |
. . . 4
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
19 | | cnrest2r 20901 |
. . . 4
⊢ (𝐶 ∈ Top → ((𝐿 ↾t 𝑊) Cn (𝐶 ↾t (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))) ⊆ ((𝐿 ↾t 𝑊) Cn 𝐶)) |
20 | 17, 18, 19 | 3syl 18 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝐿 ↾t 𝑊) Cn (𝐶 ↾t (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))) ⊆ ((𝐿 ↾t 𝑊) Cn 𝐶)) |
21 | | retopon 22377 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
22 | 12, 21 | eqeltri 2684 |
. . . . 5
⊢ 𝐿 ∈
(TopOn‘ℝ) |
23 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁)) |
24 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14 | cvmliftlem2 30522 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑊 ⊆ (0[,]1)) |
25 | | unitssre 12190 |
. . . . . 6
⊢ (0[,]1)
⊆ ℝ |
26 | 24, 25 | syl6ss 3580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑊 ⊆ ℝ) |
27 | | resttopon 20775 |
. . . . 5
⊢ ((𝐿 ∈ (TopOn‘ℝ)
∧ 𝑊 ⊆ ℝ)
→ (𝐿
↾t 𝑊)
∈ (TopOn‘𝑊)) |
28 | 22, 26, 27 | sylancr 694 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝐿 ↾t 𝑊) ∈ (TopOn‘𝑊)) |
29 | | eqid 2610 |
. . . . . . 7
⊢ (II
↾t 𝑊) =
(II ↾t 𝑊) |
30 | | iitopon 22490 |
. . . . . . . 8
⊢ II ∈
(TopOn‘(0[,]1)) |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → II ∈
(TopOn‘(0[,]1))) |
32 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝐺 ∈ (II Cn 𝐽)) |
33 | | iiuni 22492 |
. . . . . . . . . . 11
⊢ (0[,]1) =
∪ II |
34 | 33, 4 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶𝑋) |
35 | 32, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝐺:(0[,]1)⟶𝑋) |
36 | 35 | feqmptd 6159 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝐺 = (𝑧 ∈ (0[,]1) ↦ (𝐺‘𝑧))) |
37 | 36, 32 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑧 ∈ (0[,]1) ↦ (𝐺‘𝑧)) ∈ (II Cn 𝐽)) |
38 | 29, 31, 24, 37 | cnmpt1res 21289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ∈ ((II ↾t 𝑊) Cn 𝐽)) |
39 | | dfii2 22493 |
. . . . . . . . . 10
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
40 | 12 | oveq1i 6559 |
. . . . . . . . . 10
⊢ (𝐿 ↾t (0[,]1)) =
((topGen‘ran (,)) ↾t (0[,]1)) |
41 | 39, 40 | eqtr4i 2635 |
. . . . . . . . 9
⊢ II =
(𝐿 ↾t
(0[,]1)) |
42 | 41 | oveq1i 6559 |
. . . . . . . 8
⊢ (II
↾t 𝑊) =
((𝐿 ↾t
(0[,]1)) ↾t 𝑊) |
43 | | retop 22375 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Top |
44 | 12, 43 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝐿 ∈ Top |
45 | 44 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝐿 ∈ Top) |
46 | | ovex 6577 |
. . . . . . . . . 10
⊢ (0[,]1)
∈ V |
47 | 46 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0[,]1) ∈ V) |
48 | | restabs 20779 |
. . . . . . . . 9
⊢ ((𝐿 ∈ Top ∧ 𝑊 ⊆ (0[,]1) ∧ (0[,]1)
∈ V) → ((𝐿
↾t (0[,]1)) ↾t 𝑊) = (𝐿 ↾t 𝑊)) |
49 | 45, 24, 47, 48 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝐿 ↾t (0[,]1))
↾t 𝑊) =
(𝐿 ↾t
𝑊)) |
50 | 42, 49 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (II ↾t 𝑊) = (𝐿 ↾t 𝑊)) |
51 | 50 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((II ↾t 𝑊) Cn 𝐽) = ((𝐿 ↾t 𝑊) Cn 𝐽)) |
52 | 38, 51 | eleqtrd 2690 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ∈ ((𝐿 ↾t 𝑊) Cn 𝐽)) |
53 | | cvmtop2 30497 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top) |
54 | 17, 53 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝐽 ∈ Top) |
55 | 4 | toptopon 20548 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
56 | 54, 55 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝐽 ∈ (TopOn‘𝑋)) |
57 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝑊)) → 𝑀 ∈ (1...𝑁)) |
58 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝑊)) → 𝑧 ∈ 𝑊) |
59 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 57, 14, 58 | cvmliftlem3 30523 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝑊)) → (𝐺‘𝑧) ∈ (1st ‘(𝑇‘𝑀))) |
60 | 59 | anassrs 678 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑀 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝑊) → (𝐺‘𝑧) ∈ (1st ‘(𝑇‘𝑀))) |
61 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) = (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) |
62 | 60, 61 | fmptd 6292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)):𝑊⟶(1st ‘(𝑇‘𝑀))) |
63 | | frn 5966 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)):𝑊⟶(1st ‘(𝑇‘𝑀)) → ran (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ⊆ (1st ‘(𝑇‘𝑀))) |
64 | 62, 63 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ran (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ⊆ (1st ‘(𝑇‘𝑀))) |
65 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23 | cvmliftlem1 30521 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (2nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1st ‘(𝑇‘𝑀)))) |
66 | 2 | cvmsrcl 30500 |
. . . . . . . 8
⊢
((2nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1st ‘(𝑇‘𝑀))) → (1st ‘(𝑇‘𝑀)) ∈ 𝐽) |
67 | | elssuni 4403 |
. . . . . . . 8
⊢
((1st ‘(𝑇‘𝑀)) ∈ 𝐽 → (1st ‘(𝑇‘𝑀)) ⊆ ∪
𝐽) |
68 | 65, 66, 67 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (1st ‘(𝑇‘𝑀)) ⊆ ∪
𝐽) |
69 | 68, 4 | syl6sseqr 3615 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (1st ‘(𝑇‘𝑀)) ⊆ 𝑋) |
70 | | cnrest2 20900 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ran (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ⊆ (1st ‘(𝑇‘𝑀)) ∧ (1st ‘(𝑇‘𝑀)) ⊆ 𝑋) → ((𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ∈ ((𝐿 ↾t 𝑊) Cn 𝐽) ↔ (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ∈ ((𝐿 ↾t 𝑊) Cn (𝐽 ↾t (1st
‘(𝑇‘𝑀)))))) |
71 | 56, 64, 69, 70 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ∈ ((𝐿 ↾t 𝑊) Cn 𝐽) ↔ (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ∈ ((𝐿 ↾t 𝑊) Cn (𝐽 ↾t (1st
‘(𝑇‘𝑀)))))) |
72 | 52, 71 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑧 ∈ 𝑊 ↦ (𝐺‘𝑧)) ∈ ((𝐿 ↾t 𝑊) Cn (𝐽 ↾t (1st
‘(𝑇‘𝑀))))) |
73 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | cvmliftlem7 30527 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})) |
74 | | cvmcn 30498 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
75 | 3, 4 | cnf 20860 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶𝑋) |
76 | 17, 74, 75 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝐹:𝐵⟶𝑋) |
77 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐹:𝐵⟶𝑋 → 𝐹 Fn 𝐵) |
78 | | fniniseg 6246 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐵 → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}) ↔ (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁))))) |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}) ↔ (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁))))) |
80 | 73, 79 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁)))) |
81 | 80 | simpld 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵) |
82 | 80 | simprd 478 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁))) |
83 | 1 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ ℕ) |
84 | 83 | nnred 10912 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ ℝ) |
85 | | peano2rem 10227 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈
ℝ) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ ℝ) |
87 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℕ) |
88 | 86, 87 | nndivred 10946 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ ℝ) |
89 | 88 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈
ℝ*) |
90 | 84, 87 | nndivred 10946 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 / 𝑁) ∈ ℝ) |
91 | 90 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 / 𝑁) ∈
ℝ*) |
92 | 84 | ltm1d 10835 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) < 𝑀) |
93 | 87 | nnred 10912 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℝ) |
94 | 87 | nngt0d 10941 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 0 < 𝑁) |
95 | | ltdiv1 10766 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 − 1) ∈ ℝ ∧
𝑀 ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → ((𝑀 − 1) < 𝑀 ↔ ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁))) |
96 | 86, 84, 93, 94, 95 | syl112anc 1322 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) < 𝑀 ↔ ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁))) |
97 | 92, 96 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁)) |
98 | 88, 90, 97 | ltled 10064 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ≤ (𝑀 / 𝑁)) |
99 | | lbicc2 12159 |
. . . . . . . . . . . 12
⊢ ((((𝑀 − 1) / 𝑁) ∈ ℝ* ∧ (𝑀 / 𝑁) ∈ ℝ* ∧ ((𝑀 − 1) / 𝑁) ≤ (𝑀 / 𝑁)) → ((𝑀 − 1) / 𝑁) ∈ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))) |
100 | 89, 91, 98, 99 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))) |
101 | 100, 14 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ 𝑊) |
102 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14, 101 | cvmliftlem3 30523 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝐺‘((𝑀 − 1) / 𝑁)) ∈ (1st ‘(𝑇‘𝑀))) |
103 | 82, 102 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) ∈ (1st ‘(𝑇‘𝑀))) |
104 | | eqid 2610 |
. . . . . . . . 9
⊢
(℩𝑏
∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) = (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) |
105 | 2, 3, 104 | cvmsiota 30513 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ ((2nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1st ‘(𝑇‘𝑀))) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) ∈ (1st ‘(𝑇‘𝑀)))) → ((℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇‘𝑀)) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))) |
106 | 17, 65, 81, 103, 105 | syl13anc 1320 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇‘𝑀)) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))) |
107 | 106 | simpld 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇‘𝑀))) |
108 | 2 | cvmshmeo 30507 |
. . . . . 6
⊢
(((2nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1st ‘(𝑇‘𝑀))) ∧ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇‘𝑀))) → (𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐶 ↾t (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽 ↾t (1st
‘(𝑇‘𝑀))))) |
109 | 65, 107, 108 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐶 ↾t (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽 ↾t (1st
‘(𝑇‘𝑀))))) |
110 | | hmeocnvcn 21374 |
. . . . 5
⊢ ((𝐹 ↾ (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐶 ↾t (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽 ↾t (1st
‘(𝑇‘𝑀)))) → ◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐽 ↾t (1st
‘(𝑇‘𝑀))) Cn (𝐶 ↾t (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))) |
111 | 109, 110 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐽 ↾t (1st
‘(𝑇‘𝑀))) Cn (𝐶 ↾t (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))) |
112 | 28, 72, 111 | cnmpt11f 21277 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) ∈ ((𝐿 ↾t 𝑊) Cn (𝐶 ↾t (℩𝑏 ∈ (2nd
‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))) |
113 | 20, 112 | sseldd 3569 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) ∈ ((𝐿 ↾t 𝑊) Cn 𝐶)) |
114 | 16, 113 | eqeltrd 2688 |
1
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑄‘𝑀) ∈ ((𝐿 ↾t 𝑊) Cn 𝐶)) |