Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftlem15 Structured version   Visualization version   GIF version

Theorem cvmliftlem15 32570
Description: Lemma for cvmlift 32571. Discharge the assumptions of cvmliftlem14 32569. The set of all open subsets 𝑢 of the unit interval such that 𝐺𝑢 is contained in an even covering of some open set in 𝐽 is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii 23567, there is a subdivision of the closed unit interval into 𝑁 equal parts such that each part is entirely contained within one such open set of 𝐽. Then using finite choice ac6sfi 8753 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 32569. (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))
Assertion
Ref Expression
cvmliftlem15 (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Distinct variable groups:   𝑣,𝐵   𝑓,𝑘,𝑠,𝑢,𝑣,𝐹   𝑃,𝑓,𝑘,𝑢,𝑣   𝐶,𝑓,𝑘,𝑠,𝑢,𝑣   𝜑,𝑓,𝑠   𝑆,𝑓,𝑘,𝑠,𝑢,𝑣   𝑓,𝐺,𝑘,𝑠,𝑢,𝑣   𝑓,𝐽,𝑘,𝑠,𝑢,𝑣
Allowed substitution hints:   𝜑(𝑣,𝑢,𝑘)   𝐵(𝑢,𝑓,𝑘,𝑠)   𝑃(𝑠)   𝑋(𝑣,𝑢,𝑓,𝑘,𝑠)

Proof of Theorem cvmliftlem15
Dummy variables 𝑏 𝑦 𝑧 𝑎 𝑐 𝑔 𝑗 𝑚 𝑛 𝑡 𝑤 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab2 4041 . . 3 {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} ⊆ II
2 cvmliftlem.g . . . . . . . . . . 11 (𝜑𝐺 ∈ (II Cn 𝐽))
32ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → 𝐺 ∈ (II Cn 𝐽))
4 simprl 770 . . . . . . . . . 10 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → 𝑗𝐽)
5 cnima 21866 . . . . . . . . . 10 ((𝐺 ∈ (II Cn 𝐽) ∧ 𝑗𝐽) → (𝐺𝑗) ∈ II)
63, 4, 5syl2anc 587 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → (𝐺𝑗) ∈ II)
7 simplr 768 . . . . . . . . . 10 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → 𝑥 ∈ (0[,]1))
8 simprrl 780 . . . . . . . . . 10 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → (𝐺𝑥) ∈ 𝑗)
9 iiuni 23482 . . . . . . . . . . . . . 14 (0[,]1) = II
10 cvmliftlem.x . . . . . . . . . . . . . 14 𝑋 = 𝐽
119, 10cnf 21847 . . . . . . . . . . . . 13 (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶𝑋)
122, 11syl 17 . . . . . . . . . . . 12 (𝜑𝐺:(0[,]1)⟶𝑋)
1312ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → 𝐺:(0[,]1)⟶𝑋)
14 ffn 6502 . . . . . . . . . . 11 (𝐺:(0[,]1)⟶𝑋𝐺 Fn (0[,]1))
15 elpreima 6816 . . . . . . . . . . 11 (𝐺 Fn (0[,]1) → (𝑥 ∈ (𝐺𝑗) ↔ (𝑥 ∈ (0[,]1) ∧ (𝐺𝑥) ∈ 𝑗)))
1613, 14, 153syl 18 . . . . . . . . . 10 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → (𝑥 ∈ (𝐺𝑗) ↔ (𝑥 ∈ (0[,]1) ∧ (𝐺𝑥) ∈ 𝑗)))
177, 8, 16mpbir2and 712 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → 𝑥 ∈ (𝐺𝑗))
18 simprrr 781 . . . . . . . . . 10 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → (𝑆𝑗) ≠ ∅)
19 ffun 6505 . . . . . . . . . . . . 13 (𝐺:(0[,]1)⟶𝑋 → Fun 𝐺)
20 funimacnv 6423 . . . . . . . . . . . . 13 (Fun 𝐺 → (𝐺 “ (𝐺𝑗)) = (𝑗 ∩ ran 𝐺))
2113, 19, 203syl 18 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → (𝐺 “ (𝐺𝑗)) = (𝑗 ∩ ran 𝐺))
22 inss1 4189 . . . . . . . . . . . 12 (𝑗 ∩ ran 𝐺) ⊆ 𝑗
2321, 22eqsstrdi 4006 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → (𝐺 “ (𝐺𝑗)) ⊆ 𝑗)
2423ralrimivw 3178 . . . . . . . . . 10 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → ∀𝑠 ∈ (𝑆𝑗)(𝐺 “ (𝐺𝑗)) ⊆ 𝑗)
25 r19.2z 4422 . . . . . . . . . 10 (((𝑆𝑗) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆𝑗)(𝐺 “ (𝐺𝑗)) ⊆ 𝑗) → ∃𝑠 ∈ (𝑆𝑗)(𝐺 “ (𝐺𝑗)) ⊆ 𝑗)
2618, 24, 25syl2anc 587 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → ∃𝑠 ∈ (𝑆𝑗)(𝐺 “ (𝐺𝑗)) ⊆ 𝑗)
27 eleq2 2904 . . . . . . . . . . 11 (𝑢 = (𝐺𝑗) → (𝑥𝑢𝑥 ∈ (𝐺𝑗)))
28 imaeq2 5912 . . . . . . . . . . . . 13 (𝑢 = (𝐺𝑗) → (𝐺𝑢) = (𝐺 “ (𝐺𝑗)))
2928sseq1d 3983 . . . . . . . . . . . 12 (𝑢 = (𝐺𝑗) → ((𝐺𝑢) ⊆ 𝑗 ↔ (𝐺 “ (𝐺𝑗)) ⊆ 𝑗))
3029rexbidv 3290 . . . . . . . . . . 11 (𝑢 = (𝐺𝑗) → (∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗 ↔ ∃𝑠 ∈ (𝑆𝑗)(𝐺 “ (𝐺𝑗)) ⊆ 𝑗))
3127, 30anbi12d 633 . . . . . . . . . 10 (𝑢 = (𝐺𝑗) → ((𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗) ↔ (𝑥 ∈ (𝐺𝑗) ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺 “ (𝐺𝑗)) ⊆ 𝑗)))
3231rspcev 3609 . . . . . . . . 9 (((𝐺𝑗) ∈ II ∧ (𝑥 ∈ (𝐺𝑗) ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺 “ (𝐺𝑗)) ⊆ 𝑗)) → ∃𝑢 ∈ II (𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗))
336, 17, 26, 32syl12anc 835 . . . . . . . 8 (((𝜑𝑥 ∈ (0[,]1)) ∧ (𝑗𝐽 ∧ ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))) → ∃𝑢 ∈ II (𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗))
34 cvmliftlem.f . . . . . . . . . 10 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
3534adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]1)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
3612ffvelrnda 6839 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]1)) → (𝐺𝑥) ∈ 𝑋)
37 cvmliftlem.1 . . . . . . . . . 10 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
3837, 10cvmcov 32535 . . . . . . . . 9 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺𝑥) ∈ 𝑋) → ∃𝑗𝐽 ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))
3935, 36, 38syl2anc 587 . . . . . . . 8 ((𝜑𝑥 ∈ (0[,]1)) → ∃𝑗𝐽 ((𝐺𝑥) ∈ 𝑗 ∧ (𝑆𝑗) ≠ ∅))
4033, 39reximddv 3268 . . . . . . 7 ((𝜑𝑥 ∈ (0[,]1)) → ∃𝑗𝐽𝑢 ∈ II (𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗))
41 r19.42v 3342 . . . . . . . . 9 (∃𝑗𝐽 (𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗) ↔ (𝑥𝑢 ∧ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗))
4241rexbii 3242 . . . . . . . 8 (∃𝑢 ∈ II ∃𝑗𝐽 (𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗) ↔ ∃𝑢 ∈ II (𝑥𝑢 ∧ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗))
43 rexcom 3347 . . . . . . . 8 (∃𝑗𝐽𝑢 ∈ II (𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗) ↔ ∃𝑢 ∈ II ∃𝑗𝐽 (𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗))
44 elunirab 4840 . . . . . . . 8 (𝑥 {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} ↔ ∃𝑢 ∈ II (𝑥𝑢 ∧ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗))
4542, 43, 443bitr4i 306 . . . . . . 7 (∃𝑗𝐽𝑢 ∈ II (𝑥𝑢 ∧ ∃𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗) ↔ 𝑥 {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗})
4640, 45sylib 221 . . . . . 6 ((𝜑𝑥 ∈ (0[,]1)) → 𝑥 {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗})
4746ex 416 . . . . 5 (𝜑 → (𝑥 ∈ (0[,]1) → 𝑥 {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗}))
4847ssrdv 3958 . . . 4 (𝜑 → (0[,]1) ⊆ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗})
49 uniss 4832 . . . . . 6 ({𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} ⊆ II → {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} ⊆ II)
501, 49mp1i 13 . . . . 5 (𝜑 {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} ⊆ II)
5150, 9sseqtrrdi 4003 . . . 4 (𝜑 {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} ⊆ (0[,]1))
5248, 51eqssd 3969 . . 3 (𝜑 → (0[,]1) = {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗})
53 lebnumii 23567 . . 3 (({𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} ⊆ II ∧ (0[,]1) = {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗}) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣)
541, 52, 53sylancr 590 . 2 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣)
55 fzfi 13340 . . . . 5 (1...𝑛) ∈ Fin
56 imaeq2 5912 . . . . . . . . . 10 (𝑢 = 𝑣 → (𝐺𝑢) = (𝐺𝑣))
5756sseq1d 3983 . . . . . . . . 9 (𝑢 = 𝑣 → ((𝐺𝑢) ⊆ 𝑗 ↔ (𝐺𝑣) ⊆ 𝑗))
58572rexbidv 3293 . . . . . . . 8 (𝑢 = 𝑣 → (∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗 ↔ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑣) ⊆ 𝑗))
5958rexrab 3673 . . . . . . 7 (∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 ↔ ∃𝑣 ∈ II (∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣))
60 vex 3483 . . . . . . . . . . . . 13 𝑗 ∈ V
61 vex 3483 . . . . . . . . . . . . 13 𝑠 ∈ V
6260, 61op1std 7689 . . . . . . . . . . . 12 (𝑢 = ⟨𝑗, 𝑠⟩ → (1st𝑢) = 𝑗)
6362sseq2d 3984 . . . . . . . . . . 11 (𝑢 = ⟨𝑗, 𝑠⟩ → ((𝐺𝑣) ⊆ (1st𝑢) ↔ (𝐺𝑣) ⊆ 𝑗))
6463rexiunxp 5698 . . . . . . . . . 10 (∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺𝑣) ⊆ (1st𝑢) ↔ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑣) ⊆ 𝑗)
65 imass2 5952 . . . . . . . . . . . 12 ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (𝐺𝑣))
66 sstr2 3959 . . . . . . . . . . . 12 ((𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (𝐺𝑣) → ((𝐺𝑣) ⊆ (1st𝑢) → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢)))
6765, 66syl 17 . . . . . . . . . . 11 ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ((𝐺𝑣) ⊆ (1st𝑢) → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢)))
6867reximdv 3266 . . . . . . . . . 10 ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺𝑣) ⊆ (1st𝑢) → ∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢)))
6964, 68syl5bir 246 . . . . . . . . 9 ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑣) ⊆ 𝑗 → ∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢)))
7069impcom 411 . . . . . . . 8 ((∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣) → ∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢))
7170rexlimivw 3275 . . . . . . 7 (∃𝑣 ∈ II (∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣) → ∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢))
7259, 71sylbi 220 . . . . . 6 (∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢))
7372ralimi 3155 . . . . 5 (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∀𝑘 ∈ (1...𝑛)∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢))
74 fveq2 6658 . . . . . . 7 (𝑢 = (𝑔𝑘) → (1st𝑢) = (1st ‘(𝑔𝑘)))
7574sseq2d 3984 . . . . . 6 (𝑢 = (𝑔𝑘) → ((𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢) ↔ (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘))))
7675ac6sfi 8753 . . . . 5 (((1...𝑛) ∈ Fin ∧ ∀𝑘 ∈ (1...𝑛)∃𝑢 𝑗𝐽 ({𝑗} × (𝑆𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st𝑢)) → ∃𝑔(𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘))))
7755, 73, 76sylancr 590 . . . 4 (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃𝑔(𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘))))
78 cvmliftlem.b . . . . . . 7 𝐵 = 𝐶
7934ad2antrr 725 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
802ad2antrr 725 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → 𝐺 ∈ (II Cn 𝐽))
81 cvmliftlem.p . . . . . . . 8 (𝜑𝑃𝐵)
8281ad2antrr 725 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → 𝑃𝐵)
83 cvmliftlem.e . . . . . . . 8 (𝜑 → (𝐹𝑃) = (𝐺‘0))
8483ad2antrr 725 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → (𝐹𝑃) = (𝐺‘0))
85 simplr 768 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → 𝑛 ∈ ℕ)
86 simprl 770 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → 𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)))
87 sneq 4559 . . . . . . . . . . 11 (𝑗 = 𝑎 → {𝑗} = {𝑎})
88 fveq2 6658 . . . . . . . . . . 11 (𝑗 = 𝑎 → (𝑆𝑗) = (𝑆𝑎))
8987, 88xpeq12d 5573 . . . . . . . . . 10 (𝑗 = 𝑎 → ({𝑗} × (𝑆𝑗)) = ({𝑎} × (𝑆𝑎)))
9089cbviunv 4951 . . . . . . . . 9 𝑗𝐽 ({𝑗} × (𝑆𝑗)) = 𝑎𝐽 ({𝑎} × (𝑆𝑎))
91 feq3 6485 . . . . . . . . 9 ( 𝑗𝐽 ({𝑗} × (𝑆𝑗)) = 𝑎𝐽 ({𝑎} × (𝑆𝑎)) → (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ↔ 𝑔:(1...𝑛)⟶ 𝑎𝐽 ({𝑎} × (𝑆𝑎))))
9290, 91ax-mp 5 . . . . . . . 8 (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ↔ 𝑔:(1...𝑛)⟶ 𝑎𝐽 ({𝑎} × (𝑆𝑎)))
9386, 92sylib 221 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → 𝑔:(1...𝑛)⟶ 𝑎𝐽 ({𝑎} × (𝑆𝑎)))
94 simprr 772 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))
95 eqid 2824 . . . . . . 7 (topGen‘ran (,)) = (topGen‘ran (,))
96 2fveq3 6663 . . . . . . . . . . 11 (𝑡 = 𝑧 → ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡)) = ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑧)))
9796cbvmptv 5155 . . . . . . . . . 10 (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑧)))
98 eleq2 2904 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑏 → ((𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐 ↔ (𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
9998cbvriotavw 7113 . . . . . . . . . . . . . . 15 (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐) = (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)
100 fveq1 6657 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (𝑦‘((𝑤 − 1) / 𝑛)) = (𝑥‘((𝑤 − 1) / 𝑛)))
101100eleq1d 2900 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → ((𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏 ↔ (𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
102101riotabidv 7105 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏) = (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
10399, 102syl5eq 2871 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐) = (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
104103reseq2d 5840 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐)) = (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)))
105104cnveqd 5733 . . . . . . . . . . . 12 (𝑦 = 𝑥(𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐)) = (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)))
106105fveq1d 6660 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑧)) = ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧)))
107106mpteq2dv 5148 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑧))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧))))
10897, 107syl5eq 2871 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧))))
109 oveq1 7152 . . . . . . . . . . . 12 (𝑤 = 𝑚 → (𝑤 − 1) = (𝑚 − 1))
110109oveq1d 7160 . . . . . . . . . . 11 (𝑤 = 𝑚 → ((𝑤 − 1) / 𝑛) = ((𝑚 − 1) / 𝑛))
111 oveq1 7152 . . . . . . . . . . 11 (𝑤 = 𝑚 → (𝑤 / 𝑛) = (𝑚 / 𝑛))
112110, 111oveq12d 7163 . . . . . . . . . 10 (𝑤 = 𝑚 → (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) = (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)))
113 2fveq3 6663 . . . . . . . . . . . . . 14 (𝑤 = 𝑚 → (2nd ‘(𝑔𝑤)) = (2nd ‘(𝑔𝑚)))
114110fveq2d 6662 . . . . . . . . . . . . . . 15 (𝑤 = 𝑚 → (𝑥‘((𝑤 − 1) / 𝑛)) = (𝑥‘((𝑚 − 1) / 𝑛)))
115114eleq1d 2900 . . . . . . . . . . . . . 14 (𝑤 = 𝑚 → ((𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏 ↔ (𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))
116113, 115riotaeqbidv 7106 . . . . . . . . . . . . 13 (𝑤 = 𝑚 → (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏) = (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))
117116reseq2d 5840 . . . . . . . . . . . 12 (𝑤 = 𝑚 → (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)) = (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏)))
118117cnveqd 5733 . . . . . . . . . . 11 (𝑤 = 𝑚(𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)) = (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏)))
119118fveq1d 6660 . . . . . . . . . 10 (𝑤 = 𝑚 → ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧)) = ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧)))
120112, 119mpteq12dv 5137 . . . . . . . . 9 (𝑤 = 𝑚 → (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧))) = (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧))))
121108, 120cbvmpov 7238 . . . . . . . 8 (𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡)))) = (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧))))
122 seqeq2 13373 . . . . . . . 8 ((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡)))) = (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧)))) → seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})) = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})))
123121, 122ax-mp 5 . . . . . . 7 seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})) = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑔𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
124 eqid 2824 . . . . . . 7 𝑘 ∈ (1...𝑛)(seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘𝑘) = 𝑘 ∈ (1...𝑛)(seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ ((𝐹 ↾ (𝑐 ∈ (2nd ‘(𝑔𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘𝑘)
12537, 78, 10, 79, 80, 82, 84, 85, 93, 94, 95, 123, 124cvmliftlem14 32569 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘)))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
126125ex 416 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
127126exlimdv 1935 . . . 4 ((𝜑𝑛 ∈ ℕ) → (∃𝑔(𝑔:(1...𝑛)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1st ‘(𝑔𝑘))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
12877, 127syl5 34 . . 3 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
129128rexlimdva 3277 . 2 (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗𝐽𝑠 ∈ (𝑆𝑗)(𝐺𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
13054, 129mpd 15 1 (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wex 1781  wcel 2115  wne 3014  wral 3133  wrex 3134  ∃!wreu 3135  {crab 3137  Vcvv 3480  cdif 3916  cun 3917  cin 3918  wss 3919  c0 4275  𝒫 cpw 4521  {csn 4549  cop 4555   cuni 4824   ciun 4905  cmpt 5132   I cid 5446   × cxp 5540  ccnv 5541  ran crn 5543  cres 5544  cima 5545  ccom 5546  Fun wfun 6337   Fn wfn 6338  wf 6339  cfv 6343  crio 7102  (class class class)co 7145  cmpo 7147  1st c1st 7677  2nd c2nd 7678  Fincfn 8499  0cc0 10529  1c1 10530  cmin 10862   / cdiv 11289  cn 11630  (,)cioo 12731  [,]cicc 12734  ...cfz 12890  seqcseq 13369  t crest 16690  topGenctg 16707   Cn ccn 21825  Homeochmeo 22354  IIcii 23476   CovMap ccvm 32527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451  ax-inf2 9095  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7399  df-om 7571  df-1st 7679  df-2nd 7680  df-supp 7821  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-2o 8093  df-oadd 8096  df-er 8279  df-ec 8281  df-map 8398  df-ixp 8452  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-fsupp 8825  df-fi 8866  df-sup 8897  df-inf 8898  df-oi 8965  df-card 9359  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11693  df-3 11694  df-4 11695  df-5 11696  df-6 11697  df-7 11698  df-8 11699  df-9 11700  df-n0 11891  df-z 11975  df-dec 12092  df-uz 12237  df-q 12342  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ioo 12735  df-ico 12737  df-icc 12738  df-fz 12891  df-fzo 13034  df-fl 13162  df-seq 13370  df-exp 13431  df-hash 13692  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-sum 15039  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-submnd 17953  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20530  df-xmet 20531  df-met 20532  df-bl 20533  df-mopn 20534  df-cnfld 20539  df-top 21495  df-topon 21512  df-topsp 21534  df-bases 21547  df-cld 21620  df-ntr 21621  df-cls 21622  df-nei 21699  df-cn 21828  df-cnp 21829  df-cmp 21988  df-conn 22013  df-lly 22067  df-nlly 22068  df-tx 22163  df-hmeo 22356  df-xms 22923  df-ms 22924  df-tms 22925  df-ii 23478  df-htpy 23571  df-phtpy 23572  df-phtpc 23593  df-pconn 32493  df-sconn 32494  df-cvm 32528
This theorem is referenced by:  cvmlift  32571
  Copyright terms: Public domain W3C validator