Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftlem10 Structured version   Visualization version   GIF version
Theorem cvmliftlem10 34774
Description: Lemma for cvmlift 34779. The function 𝐾 is going to be our complete lifted path, formed by unioning together all the 𝑄 functions (each of which is defined on one segment [(𝑀 βˆ’ 1) / 𝑁, 𝑀 / 𝑁] of the interval). Here we prove by induction that 𝐾 is a continuous function and a lift of 𝐺 by applying cvmliftlem6 34770, cvmliftlem7 34771 (to show it is a function and a lift), cvmliftlem8 34772 (to show it is continuous), and cvmliftlem9 34773 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23120 gives that 𝐾 is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
Hypotheses
Ref Expression
cvmliftlem.1 𝑆 = (π‘˜ ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐢 βˆ– {βˆ…}) ∣ (βˆͺ 𝑠 = (◑𝐹 β€œ π‘˜) ∧ βˆ€π‘’ ∈ 𝑠 (βˆ€π‘£ ∈ (𝑠 βˆ– {𝑒})(𝑒 ∩ 𝑣) = βˆ… ∧ (𝐹 β†Ύ 𝑒) ∈ ((𝐢 β†Ύt 𝑒)Homeo(𝐽 β†Ύt π‘˜))))})
cvmliftlem.b 𝐡 = βˆͺ 𝐢
cvmliftlem.x 𝑋 = βˆͺ 𝐽
cvmliftlem.f (πœ‘ β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
cvmliftlem.g (πœ‘ β†’ 𝐺 ∈ (II Cn 𝐽))
cvmliftlem.p (πœ‘ β†’ 𝑃 ∈ 𝐡)
cvmliftlem.e (πœ‘ β†’ (πΉβ€˜π‘ƒ) = (πΊβ€˜0))
cvmliftlem.n (πœ‘ β†’ 𝑁 ∈ β„•)
cvmliftlem.t (πœ‘ β†’ 𝑇:(1...𝑁)⟢βˆͺ 𝑗 ∈ 𝐽 ({𝑗} Γ— (π‘†β€˜π‘—)))
cvmliftlem.a (πœ‘ β†’ βˆ€π‘˜ ∈ (1...𝑁)(𝐺 β€œ (((π‘˜ βˆ’ 1) / 𝑁)[,](π‘˜ / 𝑁))) βŠ† (1st β€˜(π‘‡β€˜π‘˜)))
cvmliftlem.l 𝐿 = (topGenβ€˜ran (,))
cvmliftlem.q 𝑄 = seq0((π‘₯ ∈ V, π‘š ∈ β„• ↦ (𝑧 ∈ (((π‘š βˆ’ 1) / 𝑁)[,](π‘š / 𝑁)) ↦ (β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘š))(π‘₯β€˜((π‘š βˆ’ 1) / 𝑁)) ∈ 𝑏))β€˜(πΊβ€˜π‘§)))), (( I β†Ύ β„•) βˆͺ {⟨0, {⟨0, π‘ƒβŸ©}⟩}))
cvmliftlem.k 𝐾 = βˆͺ π‘˜ ∈ (1...𝑁)(π‘„β€˜π‘˜)
cvmliftlem10.1 (πœ’ ↔ ((𝑛 ∈ β„• ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁))))))
Assertion
Ref Expression
cvmliftlem10 (πœ‘ β†’ (𝐾 ∈ ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ 𝐾) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁)))))
Distinct variable groups:   𝑣,𝑏,𝑧,𝐡   𝑗,𝑏,π‘˜,π‘š,𝑛,𝑠,𝑒,π‘₯,𝐹,𝑣,𝑧   𝑛,𝐿,𝑧   𝑃,𝑏,π‘˜,π‘š,𝑛,𝑒,𝑣,π‘₯,𝑧   𝐢,𝑏,𝑗,π‘˜,𝑛,𝑠,𝑒,𝑣,𝑧   πœ‘,𝑗,𝑛,𝑠,π‘₯,𝑧   𝑁,𝑏,π‘˜,π‘š,𝑛,𝑒,𝑣,π‘₯,𝑧   𝑆,𝑏,𝑗,π‘˜,𝑛,𝑠,𝑒,𝑣,π‘₯,𝑧   𝑗,𝑋   𝐺,𝑏,𝑗,π‘˜,π‘š,𝑛,𝑠,𝑒,𝑣,π‘₯,𝑧   𝑇,𝑏,𝑗,π‘˜,π‘š,𝑠,𝑒,𝑣,π‘₯,𝑧   𝐽,𝑏,𝑗,π‘˜,𝑛,𝑠,𝑒,𝑣,π‘₯,𝑧   𝑄,𝑏,π‘˜,π‘š,𝑛,𝑒,𝑣,π‘₯,𝑧
Allowed substitution hints:   πœ‘(𝑣,𝑒,π‘˜,π‘š,𝑏)   πœ’(π‘₯,𝑧,𝑣,𝑒,𝑗,π‘˜,π‘š,𝑛,𝑠,𝑏)   𝐡(π‘₯,𝑒,𝑗,π‘˜,π‘š,𝑛,𝑠)   𝐢(π‘₯,π‘š)   𝑃(𝑗,𝑠)   𝑄(𝑗,𝑠)   𝑆(π‘š)   𝑇(𝑛)   𝐽(π‘š)   𝐾(π‘₯,𝑧,𝑣,𝑒,𝑗,π‘˜,π‘š,𝑛,𝑠,𝑏)   𝐿(π‘₯,𝑣,𝑒,𝑗,π‘˜,π‘š,𝑠,𝑏)   𝑁(𝑗,𝑠)   𝑋(π‘₯,𝑧,𝑣,𝑒,π‘˜,π‘š,𝑛,𝑠,𝑏)
Proof of Theorem cvmliftlem10
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 cvmliftlem.n . . . 4 (πœ‘ β†’ 𝑁 ∈ β„•)
2 nnuz 12862 . . . 4 β„• = (β„€β‰₯β€˜1)
31, 2eleqtrdi 2835 . . 3 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜1))
4 eluzfz2 13506 . . 3 (𝑁 ∈ (β„€β‰₯β€˜1) β†’ 𝑁 ∈ (1...𝑁))
53, 4syl 17 . 2 (πœ‘ β†’ 𝑁 ∈ (1...𝑁))
6 eleq1 2813 . . . . . 6 (𝑦 = 1 β†’ (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7 oveq2 7409 . . . . . . . . . . 11 (𝑦 = 1 β†’ (1...𝑦) = (1...1))
8 1z 12589 . . . . . . . . . . . 12 1 ∈ β„€
9 fzsn 13540 . . . . . . . . . . . 12 (1 ∈ β„€ β†’ (1...1) = {1})
108, 9ax-mp 5 . . . . . . . . . . 11 (1...1) = {1}
117, 10eqtrdi 2780 . . . . . . . . . 10 (𝑦 = 1 β†’ (1...𝑦) = {1})
1211iuneq1d 5014 . . . . . . . . 9 (𝑦 = 1 β†’ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) = βˆͺ π‘˜ ∈ {1} (π‘„β€˜π‘˜))
13 1ex 11207 . . . . . . . . . 10 1 ∈ V
14 fveq2 6881 . . . . . . . . . 10 (π‘˜ = 1 β†’ (π‘„β€˜π‘˜) = (π‘„β€˜1))
1513, 14iunxsn 5084 . . . . . . . . 9 βˆͺ π‘˜ ∈ {1} (π‘„β€˜π‘˜) = (π‘„β€˜1)
1612, 15eqtrdi 2780 . . . . . . . 8 (𝑦 = 1 β†’ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) = (π‘„β€˜1))
17 oveq1 7408 . . . . . . . . . . 11 (𝑦 = 1 β†’ (𝑦 / 𝑁) = (1 / 𝑁))
1817oveq2d 7417 . . . . . . . . . 10 (𝑦 = 1 β†’ (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
1918oveq2d 7417 . . . . . . . . 9 (𝑦 = 1 β†’ (𝐿 β†Ύt (0[,](𝑦 / 𝑁))) = (𝐿 β†Ύt (0[,](1 / 𝑁))))
2019oveq1d 7416 . . . . . . . 8 (𝑦 = 1 β†’ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) = ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢))
2116, 20eleq12d 2819 . . . . . . 7 (𝑦 = 1 β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ↔ (π‘„β€˜1) ∈ ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢)))
2216coeq2d 5852 . . . . . . . 8 (𝑦 = 1 β†’ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐹 ∘ (π‘„β€˜1)))
2318reseq2d 5971 . . . . . . . 8 (𝑦 = 1 β†’ (𝐺 β†Ύ (0[,](𝑦 / 𝑁))) = (𝐺 β†Ύ (0[,](1 / 𝑁))))
2422, 23eqeq12d 2740 . . . . . . 7 (𝑦 = 1 β†’ ((𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (0[,](1 / 𝑁)))))
2521, 24anbi12d 630 . . . . . 6 (𝑦 = 1 β†’ ((βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁)))) ↔ ((π‘„β€˜1) ∈ ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (0[,](1 / 𝑁))))))
266, 25imbi12d 344 . . . . 5 (𝑦 = 1 β†’ ((𝑦 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) β†’ ((π‘„β€˜1) ∈ ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (0[,](1 / 𝑁)))))))
2726imbi2d 340 . . . 4 (𝑦 = 1 β†’ ((πœ‘ β†’ (𝑦 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁)))))) ↔ (πœ‘ β†’ (1 ∈ (1...𝑁) β†’ ((π‘„β€˜1) ∈ ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (0[,](1 / 𝑁))))))))
28 eleq1 2813 . . . . . 6 (𝑦 = 𝑛 β†’ (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29 oveq2 7409 . . . . . . . . 9 (𝑦 = 𝑛 β†’ (1...𝑦) = (1...𝑛))
3029iuneq1d 5014 . . . . . . . 8 (𝑦 = 𝑛 β†’ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) = βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜))
31 oveq1 7408 . . . . . . . . . . 11 (𝑦 = 𝑛 β†’ (𝑦 / 𝑁) = (𝑛 / 𝑁))
3231oveq2d 7417 . . . . . . . . . 10 (𝑦 = 𝑛 β†’ (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
3332oveq2d 7417 . . . . . . . . 9 (𝑦 = 𝑛 β†’ (𝐿 β†Ύt (0[,](𝑦 / 𝑁))) = (𝐿 β†Ύt (0[,](𝑛 / 𝑁))))
3433oveq1d 7416 . . . . . . . 8 (𝑦 = 𝑛 β†’ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) = ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢))
3530, 34eleq12d 2819 . . . . . . 7 (𝑦 = 𝑛 β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ↔ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢)))
3630coeq2d 5852 . . . . . . . 8 (𝑦 = 𝑛 β†’ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)))
3732reseq2d 5971 . . . . . . . 8 (𝑦 = 𝑛 β†’ (𝐺 β†Ύ (0[,](𝑦 / 𝑁))) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁))))
3836, 37eqeq12d 2740 . . . . . . 7 (𝑦 = 𝑛 β†’ ((𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁)))))
3935, 38anbi12d 630 . . . . . 6 (𝑦 = 𝑛 β†’ ((βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁)))) ↔ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁))))))
4028, 39imbi12d 344 . . . . 5 (𝑦 = 𝑛 β†’ ((𝑦 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁)))))))
4140imbi2d 340 . . . 4 (𝑦 = 𝑛 β†’ ((πœ‘ β†’ (𝑦 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁)))))) ↔ (πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁))))))))
42 eleq1 2813 . . . . . 6 (𝑦 = (𝑛 + 1) β†’ (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43 oveq2 7409 . . . . . . . . 9 (𝑦 = (𝑛 + 1) β†’ (1...𝑦) = (1...(𝑛 + 1)))
4443iuneq1d 5014 . . . . . . . 8 (𝑦 = (𝑛 + 1) β†’ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) = βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜))
45 oveq1 7408 . . . . . . . . . . 11 (𝑦 = (𝑛 + 1) β†’ (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
4645oveq2d 7417 . . . . . . . . . 10 (𝑦 = (𝑛 + 1) β†’ (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
4746oveq2d 7417 . . . . . . . . 9 (𝑦 = (𝑛 + 1) β†’ (𝐿 β†Ύt (0[,](𝑦 / 𝑁))) = (𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))))
4847oveq1d 7416 . . . . . . . 8 (𝑦 = (𝑛 + 1) β†’ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) = ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢))
4944, 48eleq12d 2819 . . . . . . 7 (𝑦 = (𝑛 + 1) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ↔ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢)))
5044coeq2d 5852 . . . . . . . 8 (𝑦 = (𝑛 + 1) β†’ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)))
5146reseq2d 5971 . . . . . . . 8 (𝑦 = (𝑛 + 1) β†’ (𝐺 β†Ύ (0[,](𝑦 / 𝑁))) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁))))
5250, 51eqeq12d 2740 . . . . . . 7 (𝑦 = (𝑛 + 1) β†’ ((𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁)))))
5349, 52anbi12d 630 . . . . . 6 (𝑦 = (𝑛 + 1) β†’ ((βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁)))) ↔ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁))))))
5442, 53imbi12d 344 . . . . 5 (𝑦 = (𝑛 + 1) β†’ ((𝑦 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁)))))))
5554imbi2d 340 . . . 4 (𝑦 = (𝑛 + 1) β†’ ((πœ‘ β†’ (𝑦 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁)))))) ↔ (πœ‘ β†’ ((𝑛 + 1) ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁))))))))
56 eleq1 2813 . . . . . 6 (𝑦 = 𝑁 β†’ (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57 oveq2 7409 . . . . . . . . . 10 (𝑦 = 𝑁 β†’ (1...𝑦) = (1...𝑁))
5857iuneq1d 5014 . . . . . . . . 9 (𝑦 = 𝑁 β†’ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) = βˆͺ π‘˜ ∈ (1...𝑁)(π‘„β€˜π‘˜))
59 cvmliftlem.k . . . . . . . . 9 𝐾 = βˆͺ π‘˜ ∈ (1...𝑁)(π‘„β€˜π‘˜)
6058, 59eqtr4di 2782 . . . . . . . 8 (𝑦 = 𝑁 β†’ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) = 𝐾)
61 oveq1 7408 . . . . . . . . . . 11 (𝑦 = 𝑁 β†’ (𝑦 / 𝑁) = (𝑁 / 𝑁))
6261oveq2d 7417 . . . . . . . . . 10 (𝑦 = 𝑁 β†’ (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
6362oveq2d 7417 . . . . . . . . 9 (𝑦 = 𝑁 β†’ (𝐿 β†Ύt (0[,](𝑦 / 𝑁))) = (𝐿 β†Ύt (0[,](𝑁 / 𝑁))))
6463oveq1d 7416 . . . . . . . 8 (𝑦 = 𝑁 β†’ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) = ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢))
6560, 64eleq12d 2819 . . . . . . 7 (𝑦 = 𝑁 β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ↔ 𝐾 ∈ ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢)))
6660coeq2d 5852 . . . . . . . 8 (𝑦 = 𝑁 β†’ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐹 ∘ 𝐾))
6762reseq2d 5971 . . . . . . . 8 (𝑦 = 𝑁 β†’ (𝐺 β†Ύ (0[,](𝑦 / 𝑁))) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁))))
6866, 67eqeq12d 2740 . . . . . . 7 (𝑦 = 𝑁 β†’ ((𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ 𝐾) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁)))))
6965, 68anbi12d 630 . . . . . 6 (𝑦 = 𝑁 β†’ ((βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ 𝐾) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁))))))
7056, 69imbi12d 344 . . . . 5 (𝑦 = 𝑁 β†’ ((𝑦 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) β†’ (𝐾 ∈ ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ 𝐾) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁)))))))
7170imbi2d 340 . . . 4 (𝑦 = 𝑁 β†’ ((πœ‘ β†’ (𝑦 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑦 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑦)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑦 / 𝑁)))))) ↔ (πœ‘ β†’ (𝑁 ∈ (1...𝑁) β†’ (𝐾 ∈ ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ 𝐾) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁))))))))
72 eluzfz1 13505 . . . . . . . . 9 (𝑁 ∈ (β„€β‰₯β€˜1) β†’ 1 ∈ (1...𝑁))
733, 72syl 17 . . . . . . . 8 (πœ‘ β†’ 1 ∈ (1...𝑁))
74 cvmliftlem.1 . . . . . . . . 9 𝑆 = (π‘˜ ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐢 βˆ– {βˆ…}) ∣ (βˆͺ 𝑠 = (◑𝐹 β€œ π‘˜) ∧ βˆ€π‘’ ∈ 𝑠 (βˆ€π‘£ ∈ (𝑠 βˆ– {𝑒})(𝑒 ∩ 𝑣) = βˆ… ∧ (𝐹 β†Ύ 𝑒) ∈ ((𝐢 β†Ύt 𝑒)Homeo(𝐽 β†Ύt π‘˜))))})
75 cvmliftlem.b . . . . . . . . 9 𝐡 = βˆͺ 𝐢
76 cvmliftlem.x . . . . . . . . 9 𝑋 = βˆͺ 𝐽
77 cvmliftlem.f . . . . . . . . 9 (πœ‘ β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
78 cvmliftlem.g . . . . . . . . 9 (πœ‘ β†’ 𝐺 ∈ (II Cn 𝐽))
79 cvmliftlem.p . . . . . . . . 9 (πœ‘ β†’ 𝑃 ∈ 𝐡)
80 cvmliftlem.e . . . . . . . . 9 (πœ‘ β†’ (πΉβ€˜π‘ƒ) = (πΊβ€˜0))
81 cvmliftlem.t . . . . . . . . 9 (πœ‘ β†’ 𝑇:(1...𝑁)⟢βˆͺ 𝑗 ∈ 𝐽 ({𝑗} Γ— (π‘†β€˜π‘—)))
82 cvmliftlem.a . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘˜ ∈ (1...𝑁)(𝐺 β€œ (((π‘˜ βˆ’ 1) / 𝑁)[,](π‘˜ / 𝑁))) βŠ† (1st β€˜(π‘‡β€˜π‘˜)))
83 cvmliftlem.l . . . . . . . . 9 𝐿 = (topGenβ€˜ran (,))
84 cvmliftlem.q . . . . . . . . 9 𝑄 = seq0((π‘₯ ∈ V, π‘š ∈ β„• ↦ (𝑧 ∈ (((π‘š βˆ’ 1) / 𝑁)[,](π‘š / 𝑁)) ↦ (β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘š))(π‘₯β€˜((π‘š βˆ’ 1) / 𝑁)) ∈ 𝑏))β€˜(πΊβ€˜π‘§)))), (( I β†Ύ β„•) βˆͺ {⟨0, {⟨0, π‘ƒβŸ©}⟩}))
85 eqid 2724 . . . . . . . . 9 (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁)) = (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))
8674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem8 34772 . . . . . . . 8 ((πœ‘ ∧ 1 ∈ (1...𝑁)) β†’ (π‘„β€˜1) ∈ ((𝐿 β†Ύt (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐢))
8773, 86mpdan 684 . . . . . . 7 (πœ‘ β†’ (π‘„β€˜1) ∈ ((𝐿 β†Ύt (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐢))
88 1m1e0 12281 . . . . . . . . . . . 12 (1 βˆ’ 1) = 0
8988oveq1i 7411 . . . . . . . . . . 11 ((1 βˆ’ 1) / 𝑁) = (0 / 𝑁)
901nncnd 12225 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„‚)
911nnne0d 12259 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 β‰  0)
9290, 91div0d 11986 . . . . . . . . . . 11 (πœ‘ β†’ (0 / 𝑁) = 0)
9389, 92eqtrid 2776 . . . . . . . . . 10 (πœ‘ β†’ ((1 βˆ’ 1) / 𝑁) = 0)
9493oveq1d 7416 . . . . . . . . 9 (πœ‘ β†’ (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
9594oveq2d 7417 . . . . . . . 8 (πœ‘ β†’ (𝐿 β†Ύt (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))) = (𝐿 β†Ύt (0[,](1 / 𝑁))))
9695oveq1d 7416 . . . . . . 7 (πœ‘ β†’ ((𝐿 β†Ύt (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐢) = ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢))
9787, 96eleqtrd 2827 . . . . . 6 (πœ‘ β†’ (π‘„β€˜1) ∈ ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢))
98 simpr 484 . . . . . . . . . 10 ((πœ‘ ∧ 1 ∈ (1...𝑁)) β†’ 1 ∈ (1...𝑁))
9974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem7 34771 . . . . . . . . . 10 ((πœ‘ ∧ 1 ∈ (1...𝑁)) β†’ ((π‘„β€˜(1 βˆ’ 1))β€˜((1 βˆ’ 1) / 𝑁)) ∈ (◑𝐹 β€œ {(πΊβ€˜((1 βˆ’ 1) / 𝑁))}))
10074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99cvmliftlem6 34770 . . . . . . . . 9 ((πœ‘ ∧ 1 ∈ (1...𝑁)) β†’ ((π‘„β€˜1):(((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))⟢𝐡 ∧ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁)))))
10173, 100mpdan 684 . . . . . . . 8 (πœ‘ β†’ ((π‘„β€˜1):(((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))⟢𝐡 ∧ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁)))))
102101simprd 495 . . . . . . 7 (πœ‘ β†’ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))))
10394reseq2d 5971 . . . . . . 7 (πœ‘ β†’ (𝐺 β†Ύ (((1 βˆ’ 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 β†Ύ (0[,](1 / 𝑁))))
104102, 103eqtrd 2764 . . . . . 6 (πœ‘ β†’ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (0[,](1 / 𝑁))))
10597, 104jca 511 . . . . 5 (πœ‘ β†’ ((π‘„β€˜1) ∈ ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (0[,](1 / 𝑁)))))
106105a1d 25 . . . 4 (πœ‘ β†’ (1 ∈ (1...𝑁) β†’ ((π‘„β€˜1) ∈ ((𝐿 β†Ύt (0[,](1 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ (π‘„β€˜1)) = (𝐺 β†Ύ (0[,](1 / 𝑁))))))
107 elnnuz 12863 . . . . . . . . 9 (𝑛 ∈ β„• ↔ 𝑛 ∈ (β„€β‰₯β€˜1))
108107biimpi 215 . . . . . . . 8 (𝑛 ∈ β„• β†’ 𝑛 ∈ (β„€β‰₯β€˜1))
109108adantl 481 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ (β„€β‰₯β€˜1))
110 peano2fzr 13511 . . . . . . . 8 ((𝑛 ∈ (β„€β‰₯β€˜1) ∧ (𝑛 + 1) ∈ (1...𝑁)) β†’ 𝑛 ∈ (1...𝑁))
111110ex 412 . . . . . . 7 (𝑛 ∈ (β„€β‰₯β€˜1) β†’ ((𝑛 + 1) ∈ (1...𝑁) β†’ 𝑛 ∈ (1...𝑁)))
112109, 111syl 17 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝑛 + 1) ∈ (1...𝑁) β†’ 𝑛 ∈ (1...𝑁)))
113112imim1d 82 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝑛 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁))))) β†’ ((𝑛 + 1) ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁)))))))
114 cvmliftlem10.1 . . . . . . 7 (πœ’ ↔ ((𝑛 ∈ β„• ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁))))))
115 eqid 2724 . . . . . . . . 9 βˆͺ (𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) = βˆͺ (𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁)))
116 0re 11213 . . . . . . . . . . 11 0 ∈ ℝ
117114simplbi 497 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (𝑛 ∈ β„• ∧ (𝑛 + 1) ∈ (1...𝑁)))
118117adantl 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (𝑛 ∈ β„• ∧ (𝑛 + 1) ∈ (1...𝑁)))
119118simprd 495 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ (𝑛 + 1) ∈ (1...𝑁))
120 elfznn 13527 . . . . . . . . . . . . . 14 ((𝑛 + 1) ∈ (1...𝑁) β†’ (𝑛 + 1) ∈ β„•)
121119, 120syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ (𝑛 + 1) ∈ β„•)
122121nnred 12224 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (𝑛 + 1) ∈ ℝ)
1231adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ 𝑁 ∈ β„•)
124122, 123nndivred 12263 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((𝑛 + 1) / 𝑁) ∈ ℝ)
125 iccssre 13403 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) β†’ (0[,]((𝑛 + 1) / 𝑁)) βŠ† ℝ)
126116, 124, 125sylancr 586 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (0[,]((𝑛 + 1) / 𝑁)) βŠ† ℝ)
127117simpld 494 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑛 ∈ β„•)
128127adantl 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ 𝑛 ∈ β„•)
129128nnred 12224 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ 𝑛 ∈ ℝ)
130129, 123nndivred 12263 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) ∈ ℝ)
131 icccld 24605 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) β†’ (0[,](𝑛 / 𝑁)) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
132116, 130, 131sylancr 586 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ (0[,](𝑛 / 𝑁)) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
13383fveq2i 6884 . . . . . . . . . . 11 (Clsdβ€˜πΏ) = (Clsdβ€˜(topGenβ€˜ran (,)))
134132, 133eleqtrrdi 2836 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (0[,](𝑛 / 𝑁)) ∈ (Clsdβ€˜πΏ))
135 ssun1 4164 . . . . . . . . . . 11 (0[,](𝑛 / 𝑁)) βŠ† ((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136116a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ 0 ∈ ℝ)
137128nnnn0d 12529 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ 𝑛 ∈ β„•0)
138137nn0ge0d 12532 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ 0 ≀ 𝑛)
139123nnred 12224 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ 𝑁 ∈ ℝ)
140123nngt0d 12258 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ 0 < 𝑁)
141 divge0 12080 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℝ ∧ 0 ≀ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ 0 ≀ (𝑛 / 𝑁))
142129, 138, 139, 140, 141syl22anc 836 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ 0 ≀ (𝑛 / 𝑁))
143129ltp1d 12141 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ 𝑛 < (𝑛 + 1))
144 ltdiv1 12075 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
145129, 122, 139, 140, 144syl112anc 1371 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
146143, 145mpbid 231 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
147130, 124, 146ltled 11359 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁))
148 elicc2 13386 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) β†’ ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≀ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁))))
149116, 124, 148sylancr 586 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≀ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁))))
150130, 142, 147, 149mpbir3and 1339 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)))
151 iccsplit 13459 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ ∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) β†’ (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
152136, 124, 150, 151syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
153135, 152sseqtrrid 4027 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (0[,](𝑛 / 𝑁)) βŠ† (0[,]((𝑛 + 1) / 𝑁)))
154 uniretop 24601 . . . . . . . . . . . 12 ℝ = βˆͺ (topGenβ€˜ran (,))
15583unieqi 4911 . . . . . . . . . . . 12 βˆͺ 𝐿 = βˆͺ (topGenβ€˜ran (,))
156154, 155eqtr4i 2755 . . . . . . . . . . 11 ℝ = βˆͺ 𝐿
157156restcldi 22999 . . . . . . . . . 10 (((0[,]((𝑛 + 1) / 𝑁)) βŠ† ℝ ∧ (0[,](𝑛 / 𝑁)) ∈ (Clsdβ€˜πΏ) ∧ (0[,](𝑛 / 𝑁)) βŠ† (0[,]((𝑛 + 1) / 𝑁))) β†’ (0[,](𝑛 / 𝑁)) ∈ (Clsdβ€˜(𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁)))))
158126, 134, 153, 157syl3anc 1368 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ (0[,](𝑛 / 𝑁)) ∈ (Clsdβ€˜(𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁)))))
159 icccld 24605 . . . . . . . . . . . 12 (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) β†’ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
160130, 124, 159syl2anc 583 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsdβ€˜(topGenβ€˜ran (,))))
161160, 133eleqtrrdi 2836 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsdβ€˜πΏ))
162 ssun2 4165 . . . . . . . . . . 11 ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) βŠ† ((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163162, 152sseqtrrid 4027 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) βŠ† (0[,]((𝑛 + 1) / 𝑁)))
164156restcldi 22999 . . . . . . . . . 10 (((0[,]((𝑛 + 1) / 𝑁)) βŠ† ℝ ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsdβ€˜πΏ) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) βŠ† (0[,]((𝑛 + 1) / 𝑁))) β†’ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsdβ€˜(𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁)))))
165126, 161, 163, 164syl3anc 1368 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsdβ€˜(𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁)))))
166 retop 24600 . . . . . . . . . . . 12 (topGenβ€˜ran (,)) ∈ Top
16783, 166eqeltri 2821 . . . . . . . . . . 11 𝐿 ∈ Top
168156restuni 22988 . . . . . . . . . . 11 ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) βŠ† ℝ) β†’ (0[,]((𝑛 + 1) / 𝑁)) = βˆͺ (𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))))
169167, 126, 168sylancr 586 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (0[,]((𝑛 + 1) / 𝑁)) = βˆͺ (𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))))
170152, 169eqtr3d 2766 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ ((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = βˆͺ (𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))))
171114simprbi 496 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁)))))
172171adantl 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁)))))
173172simpld 494 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢))
174 eqid 2724 . . . . . . . . . . . . . . 15 βˆͺ (𝐿 β†Ύt (0[,](𝑛 / 𝑁))) = βˆͺ (𝐿 β†Ύt (0[,](𝑛 / 𝑁)))
175174, 75cnf 23072 . . . . . . . . . . . . . 14 (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) β†’ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜):βˆͺ (𝐿 β†Ύt (0[,](𝑛 / 𝑁)))⟢𝐡)
176173, 175syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜):βˆͺ (𝐿 β†Ύt (0[,](𝑛 / 𝑁)))⟢𝐡)
177 iccssre 13403 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) β†’ (0[,](𝑛 / 𝑁)) βŠ† ℝ)
178116, 130, 177sylancr 586 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (0[,](𝑛 / 𝑁)) βŠ† ℝ)
179156restuni 22988 . . . . . . . . . . . . . . 15 ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) βŠ† ℝ) β†’ (0[,](𝑛 / 𝑁)) = βˆͺ (𝐿 β†Ύt (0[,](𝑛 / 𝑁))))
180167, 178, 179sylancr 586 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ (0[,](𝑛 / 𝑁)) = βˆͺ (𝐿 β†Ύt (0[,](𝑛 / 𝑁))))
181180feq2d 6693 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜):(0[,](𝑛 / 𝑁))⟢𝐡 ↔ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜):βˆͺ (𝐿 β†Ύt (0[,](𝑛 / 𝑁)))⟢𝐡))
182176, 181mpbird 257 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜):(0[,](𝑛 / 𝑁))⟢𝐡)
183 eqid 2724 . . . . . . . . . . . . . . . 16 ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
184 simpr 484 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑛 + 1) ∈ (1...𝑁)) β†’ (𝑛 + 1) ∈ (1...𝑁))
18574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem7 34771 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑛 + 1) ∈ (1...𝑁)) β†’ ((π‘„β€˜((𝑛 + 1) βˆ’ 1))β€˜(((𝑛 + 1) βˆ’ 1) / 𝑁)) ∈ (◑𝐹 β€œ {(πΊβ€˜(((𝑛 + 1) βˆ’ 1) / 𝑁))}))
18674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185cvmliftlem6 34770 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑛 + 1) ∈ (1...𝑁)) β†’ ((π‘„β€˜(𝑛 + 1)):((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡 ∧ (𝐹 ∘ (π‘„β€˜(𝑛 + 1))) = (𝐺 β†Ύ ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
187119, 186syldan 590 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜(𝑛 + 1)):((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡 ∧ (𝐹 ∘ (π‘„β€˜(𝑛 + 1))) = (𝐺 β†Ύ ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
188187simpld 494 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ (π‘„β€˜(𝑛 + 1)):((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡)
189128nncnd 12225 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ’) β†’ 𝑛 ∈ β„‚)
190 ax-1cn 11164 . . . . . . . . . . . . . . . . 17 1 ∈ β„‚
191 pncan 11463 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((𝑛 + 1) βˆ’ 1) = 𝑛)
192189, 190, 191sylancl 585 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ’) β†’ ((𝑛 + 1) βˆ’ 1) = 𝑛)
193192oveq1d 7416 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (((𝑛 + 1) βˆ’ 1) / 𝑁) = (𝑛 / 𝑁))
194193oveq1d 7416 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195194feq2d 6693 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜(𝑛 + 1)):((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡 ↔ (π‘„β€˜(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡))
196188, 195mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (π‘„β€˜(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡)
197176ffund 6711 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ’) β†’ Fun βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜))
198128, 108syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ πœ’) β†’ 𝑛 ∈ (β„€β‰₯β€˜1))
199 eluzfz2 13506 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (β„€β‰₯β€˜1) β†’ 𝑛 ∈ (1...𝑛))
200198, 199syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ πœ’) β†’ 𝑛 ∈ (1...𝑛))
201 fveq2 6881 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑛 β†’ (π‘„β€˜π‘˜) = (π‘„β€˜π‘›))
202201ssiun2s 5041 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑛) β†’ (π‘„β€˜π‘›) βŠ† βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜))
203200, 202syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ’) β†’ (π‘„β€˜π‘›) βŠ† βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜))
204 peano2rem 11524 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℝ β†’ (𝑛 βˆ’ 1) ∈ ℝ)
205129, 204syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ πœ’) β†’ (𝑛 βˆ’ 1) ∈ ℝ)
206205, 123nndivred 12263 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ πœ’) β†’ ((𝑛 βˆ’ 1) / 𝑁) ∈ ℝ)
207206rexrd 11261 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ πœ’) β†’ ((𝑛 βˆ’ 1) / 𝑁) ∈ ℝ*)
208130rexrd 11261 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) ∈ ℝ*)
209129ltm1d 12143 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ πœ’) β†’ (𝑛 βˆ’ 1) < 𝑛)
210 ltdiv1 12075 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 βˆ’ 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ ((𝑛 βˆ’ 1) < 𝑛 ↔ ((𝑛 βˆ’ 1) / 𝑁) < (𝑛 / 𝑁)))
211205, 129, 139, 140, 210syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ πœ’) β†’ ((𝑛 βˆ’ 1) < 𝑛 ↔ ((𝑛 βˆ’ 1) / 𝑁) < (𝑛 / 𝑁)))
212209, 211mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ πœ’) β†’ ((𝑛 βˆ’ 1) / 𝑁) < (𝑛 / 𝑁))
213206, 130, 212ltled 11359 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ πœ’) β†’ ((𝑛 βˆ’ 1) / 𝑁) ≀ (𝑛 / 𝑁))
214 ubicc2 13439 . . . . . . . . . . . . . . . . . . . 20 ((((𝑛 βˆ’ 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 βˆ’ 1) / 𝑁) ≀ (𝑛 / 𝑁)) β†’ (𝑛 / 𝑁) ∈ (((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁)))
215207, 208, 213, 214syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) ∈ (((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁)))
216198, 119, 110syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ πœ’) β†’ 𝑛 ∈ (1...𝑁))
217 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁))
218 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑛 ∈ (1...𝑁))
21974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217cvmliftlem7 34771 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘„β€˜(𝑛 βˆ’ 1))β€˜((𝑛 βˆ’ 1) / 𝑁)) ∈ (◑𝐹 β€œ {(πΊβ€˜((𝑛 βˆ’ 1) / 𝑁))}))
22074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219cvmliftlem6 34770 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘„β€˜π‘›):(((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁))⟢𝐡 ∧ (𝐹 ∘ (π‘„β€˜π‘›)) = (𝐺 β†Ύ (((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁)))))
221216, 220syldan 590 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜π‘›):(((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁))⟢𝐡 ∧ (𝐹 ∘ (π‘„β€˜π‘›)) = (𝐺 β†Ύ (((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁)))))
222221simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ πœ’) β†’ (π‘„β€˜π‘›):(((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁))⟢𝐡)
223222fdmd 6718 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ πœ’) β†’ dom (π‘„β€˜π‘›) = (((𝑛 βˆ’ 1) / 𝑁)[,](𝑛 / 𝑁)))
224215, 223eleqtrrd 2828 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) ∈ dom (π‘„β€˜π‘›))
225 funssfv 6902 . . . . . . . . . . . . . . . . . 18 ((Fun βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∧ (π‘„β€˜π‘›) βŠ† βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∧ (𝑛 / 𝑁) ∈ dom (π‘„β€˜π‘›)) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)β€˜(𝑛 / 𝑁)) = ((π‘„β€˜π‘›)β€˜(𝑛 / 𝑁)))
226197, 203, 224, 225syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)β€˜(𝑛 / 𝑁)) = ((π‘„β€˜π‘›)β€˜(𝑛 / 𝑁)))
227192fveq2d 6885 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ’) β†’ (π‘„β€˜((𝑛 + 1) βˆ’ 1)) = (π‘„β€˜π‘›))
228227, 193fveq12d 6888 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜((𝑛 + 1) βˆ’ 1))β€˜(((𝑛 + 1) βˆ’ 1) / 𝑁)) = ((π‘„β€˜π‘›)β€˜(𝑛 / 𝑁)))
22974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84cvmliftlem9 34773 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑛 + 1) ∈ (1...𝑁)) β†’ ((π‘„β€˜(𝑛 + 1))β€˜(((𝑛 + 1) βˆ’ 1) / 𝑁)) = ((π‘„β€˜((𝑛 + 1) βˆ’ 1))β€˜(((𝑛 + 1) βˆ’ 1) / 𝑁)))
230119, 229syldan 590 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜(𝑛 + 1))β€˜(((𝑛 + 1) βˆ’ 1) / 𝑁)) = ((π‘„β€˜((𝑛 + 1) βˆ’ 1))β€˜(((𝑛 + 1) βˆ’ 1) / 𝑁)))
231193fveq2d 6885 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜(𝑛 + 1))β€˜(((𝑛 + 1) βˆ’ 1) / 𝑁)) = ((π‘„β€˜(𝑛 + 1))β€˜(𝑛 / 𝑁)))
232230, 231eqtr3d 2766 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜((𝑛 + 1) βˆ’ 1))β€˜(((𝑛 + 1) βˆ’ 1) / 𝑁)) = ((π‘„β€˜(𝑛 + 1))β€˜(𝑛 / 𝑁)))
233226, 228, 2323eqtr2d 2770 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)β€˜(𝑛 / 𝑁)) = ((π‘„β€˜(𝑛 + 1))β€˜(𝑛 / 𝑁)))
234233opeq2d 4872 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ ⟨(𝑛 / 𝑁), (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)β€˜(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((π‘„β€˜(𝑛 + 1))β€˜(𝑛 / 𝑁))⟩)
235234sneqd 4632 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ {⟨(𝑛 / 𝑁), (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)β€˜(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((π‘„β€˜(𝑛 + 1))β€˜(𝑛 / 𝑁))⟩})
236182ffnd 6708 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) Fn (0[,](𝑛 / 𝑁)))
237 0xr 11258 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
238237a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ’) β†’ 0 ∈ ℝ*)
239 ubicc2 13439 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 0 ≀ (𝑛 / 𝑁)) β†’ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
240238, 208, 142, 239syl3anc 1368 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
241 fnressn 7148 . . . . . . . . . . . . . . 15 ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)β€˜(𝑛 / 𝑁))⟩})
242236, 240, 241syl2anc 583 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)β€˜(𝑛 / 𝑁))⟩})
243196ffnd 6708 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (π‘„β€˜(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
244124rexrd 11261 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ’) β†’ ((𝑛 + 1) / 𝑁) ∈ ℝ*)
245 lbicc2 13438 . . . . . . . . . . . . . . . 16 (((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁)) β†’ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
246208, 244, 147, 245syl3anc 1368 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247 fnressn 7148 . . . . . . . . . . . . . . 15 (((π‘„β€˜(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) β†’ ((π‘„β€˜(𝑛 + 1)) β†Ύ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((π‘„β€˜(𝑛 + 1))β€˜(𝑛 / 𝑁))⟩})
248243, 246, 247syl2anc 583 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜(𝑛 + 1)) β†Ύ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((π‘„β€˜(𝑛 + 1))β€˜(𝑛 / 𝑁))⟩})
249235, 242, 2483eqtr4d 2774 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ {(𝑛 / 𝑁)}) = ((π‘„β€˜(𝑛 + 1)) β†Ύ {(𝑛 / 𝑁)}))
250 df-icc 13328 . . . . . . . . . . . . . . . . 17 [,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ ≀ 𝑧 ∧ 𝑧 ≀ 𝑦)})
251 xrmaxle 13159 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 𝑧 ∈ ℝ*) β†’ (if(0 ≀ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≀ 𝑧 ↔ (0 ≀ 𝑧 ∧ (𝑛 / 𝑁) ≀ 𝑧)))
252 xrlemin 13160 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*) β†’ (𝑧 ≀ if((𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≀ (𝑛 / 𝑁) ∧ 𝑧 ≀ ((𝑛 + 1) / 𝑁))))
253250, 251, 252ixxin 13338 . . . . . . . . . . . . . . . 16 (((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*) ∧ ((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*)) β†’ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≀ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
254238, 208, 208, 244, 253syl22anc 836 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≀ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
255142iftrued 4528 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ’) β†’ if(0 ≀ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
256147iftrued 4528 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ’) β†’ if((𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
257255, 256oveq12d 7419 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ (if(0 ≀ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≀ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
258 iccid 13366 . . . . . . . . . . . . . . . 16 ((𝑛 / 𝑁) ∈ ℝ* β†’ ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
259208, 258syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ’) β†’ ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
260254, 257, 2593eqtrd 2768 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
261260reseq2d 5971 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ {(𝑛 / 𝑁)}))
262260reseq2d 5971 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ ((π‘„β€˜(𝑛 + 1)) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((π‘„β€˜(𝑛 + 1)) β†Ύ {(𝑛 / 𝑁)}))
263249, 261, 2623eqtr4d 2774 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((π‘„β€˜(𝑛 + 1)) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
264 fresaun 6752 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜):(0[,](𝑛 / 𝑁))⟢𝐡 ∧ (π‘„β€˜(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡 ∧ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((π‘„β€˜(𝑛 + 1)) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))):((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟢𝐡)
265182, 196, 263, 264syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))):((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟢𝐡)
266 fzsuc 13545 . . . . . . . . . . . . . . 15 (𝑛 ∈ (β„€β‰₯β€˜1) β†’ (1...(𝑛 + 1)) = ((1...𝑛) βˆͺ {(𝑛 + 1)}))
267198, 266syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ’) β†’ (1...(𝑛 + 1)) = ((1...𝑛) βˆͺ {(𝑛 + 1)}))
268267iuneq1d 5014 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ’) β†’ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) = βˆͺ π‘˜ ∈ ((1...𝑛) βˆͺ {(𝑛 + 1)})(π‘„β€˜π‘˜))
269 iunxun 5087 . . . . . . . . . . . . . 14 βˆͺ π‘˜ ∈ ((1...𝑛) βˆͺ {(𝑛 + 1)})(π‘„β€˜π‘˜) = (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ βˆͺ π‘˜ ∈ {(𝑛 + 1)} (π‘„β€˜π‘˜))
270 ovex 7434 . . . . . . . . . . . . . . . 16 (𝑛 + 1) ∈ V
271 fveq2 6881 . . . . . . . . . . . . . . . 16 (π‘˜ = (𝑛 + 1) β†’ (π‘„β€˜π‘˜) = (π‘„β€˜(𝑛 + 1)))
272270, 271iunxsn 5084 . . . . . . . . . . . . . . 15 βˆͺ π‘˜ ∈ {(𝑛 + 1)} (π‘„β€˜π‘˜) = (π‘„β€˜(𝑛 + 1))
273272uneq2i 4152 . . . . . . . . . . . . . 14 (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ βˆͺ π‘˜ ∈ {(𝑛 + 1)} (π‘„β€˜π‘˜)) = (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1)))
274269, 273eqtri 2752 . . . . . . . . . . . . 13 βˆͺ π‘˜ ∈ ((1...𝑛) βˆͺ {(𝑛 + 1)})(π‘„β€˜π‘˜) = (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1)))
275268, 274eqtr2di 2781 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))) = βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜))
276275feq1d 6692 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))):((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟢𝐡 ↔ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜):((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟢𝐡))
277265, 276mpbid 231 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜):((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟢𝐡)
278170feq2d 6693 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜):((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟢𝐡 ↔ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜):βˆͺ (𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁)))⟢𝐡))
279277, 278mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜):βˆͺ (𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁)))⟢𝐡)
280275reseq1d 5970 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))) β†Ύ (0[,](𝑛 / 𝑁))) = (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) β†Ύ (0[,](𝑛 / 𝑁))))
281 fresaunres1 6754 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜):(0[,](𝑛 / 𝑁))⟢𝐡 ∧ (π‘„β€˜(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡 ∧ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((π‘„β€˜(𝑛 + 1)) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) β†’ ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))) β†Ύ (0[,](𝑛 / 𝑁))) = βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜))
282182, 196, 263, 281syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))) β†Ύ (0[,](𝑛 / 𝑁))) = βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜))
283280, 282eqtr3d 2766 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) β†Ύ (0[,](𝑛 / 𝑁))) = βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜))
284167a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ 𝐿 ∈ Top)
285 ovex 7434 . . . . . . . . . . . . 13 (0[,]((𝑛 + 1) / 𝑁)) ∈ V
286285a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
287 restabs 22991 . . . . . . . . . . . 12 ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) βŠ† (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) β†’ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) β†Ύt (0[,](𝑛 / 𝑁))) = (𝐿 β†Ύt (0[,](𝑛 / 𝑁))))
288284, 153, 286, 287syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) β†Ύt (0[,](𝑛 / 𝑁))) = (𝐿 β†Ύt (0[,](𝑛 / 𝑁))))
289288oveq1d 7416 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) = ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢))
290173, 283, 2893eltr4d 2840 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) β†Ύ (0[,](𝑛 / 𝑁))) ∈ (((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢))
29174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem8 34772 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑛 + 1) ∈ (1...𝑁)) β†’ (π‘„β€˜(𝑛 + 1)) ∈ ((𝐿 β†Ύt ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐢))
292119, 291syldan 590 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ (π‘„β€˜(𝑛 + 1)) ∈ ((𝐿 β†Ύt ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐢))
293194oveq2d 7417 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (𝐿 β†Ύt ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
294293oveq1d 7416 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((𝐿 β†Ύt ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) = ((𝐿 β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐢))
295292, 294eleqtrd 2827 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (π‘„β€˜(𝑛 + 1)) ∈ ((𝐿 β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐢))
296275reseq1d 5970 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))) β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
297 fresaunres2 6753 . . . . . . . . . . . 12 ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜):(0[,](𝑛 / 𝑁))⟢𝐡 ∧ (π‘„β€˜(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟢𝐡 ∧ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((π‘„β€˜(𝑛 + 1)) β†Ύ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) β†’ ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))) β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (π‘„β€˜(𝑛 + 1)))
298182, 196, 263, 297syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1))) β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (π‘„β€˜(𝑛 + 1)))
299296, 298eqtr3d 2766 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (π‘„β€˜(𝑛 + 1)))
300 restabs 22991 . . . . . . . . . . . 12 ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) βŠ† (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) β†’ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
301284, 163, 286, 300syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
302301oveq1d 7416 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ (((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) = ((𝐿 β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐢))
303295, 299, 3023eltr4d 2840 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) β†Ύt ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐢))
304115, 75, 158, 165, 170, 279, 290, 303paste 23120 . . . . . . . 8 ((πœ‘ ∧ πœ’) β†’ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢))
305152reseq2d 5971 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 β†Ύ ((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
306172simprd 495 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁))))
307187simprd 495 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (𝐹 ∘ (π‘„β€˜(𝑛 + 1))) = (𝐺 β†Ύ ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
308194reseq2d 5971 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ’) β†’ (𝐺 β†Ύ ((((𝑛 + 1) βˆ’ 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
309307, 308eqtrd 2764 . . . . . . . . . . 11 ((πœ‘ ∧ πœ’) β†’ (𝐹 ∘ (π‘„β€˜(𝑛 + 1))) = (𝐺 β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
310306, 309uneq12d 4156 . . . . . . . . . 10 ((πœ‘ ∧ πœ’) β†’ ((𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) βˆͺ (𝐹 ∘ (π‘„β€˜(𝑛 + 1)))) = ((𝐺 β†Ύ (0[,](𝑛 / 𝑁))) βˆͺ (𝐺 β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
311 coundi 6236 . . . . . . . . . 10 (𝐹 ∘ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1)))) = ((𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) βˆͺ (𝐹 ∘ (π‘„β€˜(𝑛 + 1))))
312 resundi 5985 . . . . . . . . . 10 (𝐺 β†Ύ ((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 β†Ύ (0[,](𝑛 / 𝑁))) βˆͺ (𝐺 β†Ύ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313310, 311, 3123eqtr4g 2789 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ (𝐹 ∘ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1)))) = (𝐺 β†Ύ ((0[,](𝑛 / 𝑁)) βˆͺ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
314275coeq2d 5852 . . . . . . . . 9 ((πœ‘ ∧ πœ’) β†’ (𝐹 ∘ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) βˆͺ (π‘„β€˜(𝑛 + 1)))) = (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)))
315305, 313, 3143eqtr2rd 2771 . . . . . . . 8 ((πœ‘ ∧ πœ’) β†’ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁))))
316304, 315jca 511 . . . . . . 7 ((πœ‘ ∧ πœ’) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁)))))
317114, 316sylan2br 594 . . . . . 6 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁)))))) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁)))))
318317expr 456 . . . . 5 ((πœ‘ ∧ (𝑛 ∈ β„• ∧ (𝑛 + 1) ∈ (1...𝑁))) β†’ ((βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁)))) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁))))))
319113, 318animpimp2impd 843 . . . 4 (𝑛 ∈ β„• β†’ ((πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,](𝑛 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...𝑛)(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,](𝑛 / 𝑁)))))) β†’ (πœ‘ β†’ ((𝑛 + 1) ∈ (1...𝑁) β†’ (βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜) ∈ ((𝐿 β†Ύt (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ βˆͺ π‘˜ ∈ (1...(𝑛 + 1))(π‘„β€˜π‘˜)) = (𝐺 β†Ύ (0[,]((𝑛 + 1) / 𝑁))))))))
32027, 41, 55, 71, 106, 319nnind 12227 . . 3 (𝑁 ∈ β„• β†’ (πœ‘ β†’ (𝑁 ∈ (1...𝑁) β†’ (𝐾 ∈ ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ 𝐾) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁)))))))
3211, 320mpcom 38 . 2 (πœ‘ β†’ (𝑁 ∈ (1...𝑁) β†’ (𝐾 ∈ ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ 𝐾) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁))))))
3225, 321mpd 15 1 (πœ‘ β†’ (𝐾 ∈ ((𝐿 β†Ύt (0[,](𝑁 / 𝑁))) Cn 𝐢) ∧ (𝐹 ∘ 𝐾) = (𝐺 β†Ύ (0[,](𝑁 / 𝑁)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3053  {crab 3424  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  ifcif 4520  π’« cpw 4594  {csn 4620  βŸ¨cop 4626  βˆͺ cuni 4899  βˆͺ ciun 4987   class class class wbr 5138   ↦ cmpt 5221   I cid 5563   Γ— cxp 5664  β—‘ccnv 5665  dom cdm 5666  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669   ∘ ccom 5670  Fun wfun 6527   Fn wfn 6528  βŸΆwf 6529  β€˜cfv 6533  β„©crio 7356  (class class class)co 7401   ∈ cmpo 7403  1st c1st 7966  2nd c2nd 7967  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109  β„*cxr 11244   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441   / cdiv 11868  β„•cn 12209  β„€cz 12555  β„€β‰₯cuz 12819  (,)cioo 13321  [,]cicc 13324  ...cfz 13481  seqcseq 13963   β†Ύt crest 17365  topGenctg 17382  Topctop 22717  Clsdccld 22842   Cn ccn 23050  Homeochmeo 23579  IIcii 24717   CovMap ccvm 34735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fi 9402  df-sup 9433  df-inf 9434  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-icc 13328  df-fz 13482  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-rest 17367  df-topgen 17388  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-top 22718  df-topon 22735  df-bases 22771  df-cld 22845  df-cn 23053  df-hmeo 23581  df-ii 24719  df-cvm 34736
This theorem is referenced by:  cvmliftlem11  34775
  Copyright terms: Public domain W3C validator