Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ptrecube Structured version   Visualization version   GIF version

Theorem ptrecube 36107
Description: Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.)
Hypotheses
Ref Expression
ptrecube.r 𝑅 = (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))}))
ptrecube.d 𝐷 = ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))
Assertion
Ref Expression
ptrecube ((𝑆 ∈ 𝑅 ∧ 𝑃 ∈ 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆)
Distinct variable groups:   𝑛,𝑑,𝑁   𝑃,𝑑,𝑛   𝑆,𝑑,𝑛
Allowed substitution hints:   𝐷(𝑛,𝑑)   𝑅(𝑛,𝑑)

Proof of Theorem ptrecube
Dummy variables 𝑔 β„Ž 𝑀 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptrecube.r . . . 4 𝑅 = (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))}))
2 fzfi 13884 . . . . 5 (1...𝑁) ∈ Fin
3 retop 24141 . . . . . 6 (topGenβ€˜ran (,)) ∈ Top
4 fnconstg 6735 . . . . . 6 ((topGenβ€˜ran (,)) ∈ Top β†’ ((1...𝑁) Γ— {(topGenβ€˜ran (,))}) Fn (1...𝑁))
53, 4ax-mp 5 . . . . 5 ((1...𝑁) Γ— {(topGenβ€˜ran (,))}) Fn (1...𝑁)
6 eqid 2737 . . . . . 6 {π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))} = {π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))}
76ptval 22937 . . . . 5 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) Γ— {(topGenβ€˜ran (,))}) Fn (1...𝑁)) β†’ (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) = (topGenβ€˜{π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))}))
82, 5, 7mp2an 691 . . . 4 (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) = (topGenβ€˜{π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))})
91, 8eqtri 2765 . . 3 𝑅 = (topGenβ€˜{π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))})
109eleq2i 2830 . 2 (𝑆 ∈ 𝑅 ↔ 𝑆 ∈ (topGenβ€˜{π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))}))
11 tg2 22331 . . 3 ((𝑆 ∈ (topGenβ€˜{π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))}) ∧ 𝑃 ∈ 𝑆) β†’ βˆƒπ‘§ ∈ {π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))} (𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆))
126elpt 22939 . . . . 5 (𝑧 ∈ {π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))} ↔ βˆƒπ‘”((𝑔 Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑧)(π‘”β€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ 𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›)))
13 fvex 6860 . . . . . . . . . . . . . . 15 (topGenβ€˜ran (,)) ∈ V
1413fvconst2 7158 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) = (topGenβ€˜ran (,)))
1514eleq2d 2824 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) β†’ ((π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ↔ (π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,))))
1615ralbiia 3095 . . . . . . . . . . . 12 (βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ↔ βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)))
17 elixp2 8846 . . . . . . . . . . . . . 14 (𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) ↔ (𝑃 ∈ V ∧ 𝑃 Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)))
1817simp3bi 1148 . . . . . . . . . . . . 13 (𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) β†’ βˆ€π‘› ∈ (1...𝑁)(π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›))
19 r19.26 3115 . . . . . . . . . . . . . 14 (βˆ€π‘› ∈ (1...𝑁)((π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ (π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) ↔ (βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ βˆ€π‘› ∈ (1...𝑁)(π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)))
20 uniretop 24142 . . . . . . . . . . . . . . . . . . . . 21 ℝ = βˆͺ (topGenβ€˜ran (,))
2120eltopss 22272 . . . . . . . . . . . . . . . . . . . 20 (((topGenβ€˜ran (,)) ∈ Top ∧ (π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,))) β†’ (π‘”β€˜π‘›) βŠ† ℝ)
223, 21mpan 689 . . . . . . . . . . . . . . . . . . 19 ((π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) β†’ (π‘”β€˜π‘›) βŠ† ℝ)
2322sselda 3949 . . . . . . . . . . . . . . . . . 18 (((π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ (π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) β†’ (π‘ƒβ€˜π‘›) ∈ ℝ)
24 ptrecube.d . . . . . . . . . . . . . . . . . . . 20 𝐷 = ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))
2524rexmet 24170 . . . . . . . . . . . . . . . . . . 19 𝐷 ∈ (∞Metβ€˜β„)
26 eqid 2737 . . . . . . . . . . . . . . . . . . . . 21 (MetOpenβ€˜π·) = (MetOpenβ€˜π·)
2724, 26tgioo 24175 . . . . . . . . . . . . . . . . . . . 20 (topGenβ€˜ran (,)) = (MetOpenβ€˜π·)
2827mopni2 23865 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (∞Metβ€˜β„) ∧ (π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ (π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) β†’ βˆƒπ‘¦ ∈ ℝ+ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›))
2925, 28mp3an1 1449 . . . . . . . . . . . . . . . . . 18 (((π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ (π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) β†’ βˆƒπ‘¦ ∈ ℝ+ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›))
30 r19.42v 3188 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘¦ ∈ ℝ+ ((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›)) ↔ ((π‘ƒβ€˜π‘›) ∈ ℝ ∧ βˆƒπ‘¦ ∈ ℝ+ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›)))
3123, 29, 30sylanbrc 584 . . . . . . . . . . . . . . . . 17 (((π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ (π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) β†’ βˆƒπ‘¦ ∈ ℝ+ ((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›)))
3231ralimi 3087 . . . . . . . . . . . . . . . 16 (βˆ€π‘› ∈ (1...𝑁)((π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ (π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) β†’ βˆ€π‘› ∈ (1...𝑁)βˆƒπ‘¦ ∈ ℝ+ ((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›)))
33 oveq2 7370 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (β„Žβ€˜π‘›) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) = ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)))
3433sseq1d 3980 . . . . . . . . . . . . . . . . . 18 (𝑦 = (β„Žβ€˜π‘›) β†’ (((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›) ↔ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›)))
3534anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑦 = (β„Žβ€˜π‘›) β†’ (((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›)) ↔ ((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›))))
3635ac6sfi 9238 . . . . . . . . . . . . . . . 16 (((1...𝑁) ∈ Fin ∧ βˆ€π‘› ∈ (1...𝑁)βˆƒπ‘¦ ∈ ℝ+ ((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑦) βŠ† (π‘”β€˜π‘›))) β†’ βˆƒβ„Ž(β„Ž:(1...𝑁)βŸΆβ„+ ∧ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›))))
372, 32, 36sylancr 588 . . . . . . . . . . . . . . 15 (βˆ€π‘› ∈ (1...𝑁)((π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ (π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) β†’ βˆƒβ„Ž(β„Ž:(1...𝑁)βŸΆβ„+ ∧ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›))))
38 1rp 12926 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ+
3938a1i 11 . . . . . . . . . . . . . . . . . . 19 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ (1...𝑁) = βˆ…) β†’ 1 ∈ ℝ+)
40 frn 6680 . . . . . . . . . . . . . . . . . . . . 21 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ ran β„Ž βŠ† ℝ+)
4140adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ Β¬ (1...𝑁) = βˆ…) β†’ ran β„Ž βŠ† ℝ+)
42 ffn 6673 . . . . . . . . . . . . . . . . . . . . . . . 24 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ β„Ž Fn (1...𝑁))
43 fnfi 9132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((β„Ž Fn (1...𝑁) ∧ (1...𝑁) ∈ Fin) β†’ β„Ž ∈ Fin)
4442, 2, 43sylancl 587 . . . . . . . . . . . . . . . . . . . . . . 23 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ β„Ž ∈ Fin)
45 rnfi 9286 . . . . . . . . . . . . . . . . . . . . . . 23 (β„Ž ∈ Fin β†’ ran β„Ž ∈ Fin)
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ ran β„Ž ∈ Fin)
4746adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ Β¬ (1...𝑁) = βˆ…) β†’ ran β„Ž ∈ Fin)
48 dm0rn0 5885 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom β„Ž = βˆ… ↔ ran β„Ž = βˆ…)
49 fdm 6682 . . . . . . . . . . . . . . . . . . . . . . . . 25 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ dom β„Ž = (1...𝑁))
5049eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . 24 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ (dom β„Ž = βˆ… ↔ (1...𝑁) = βˆ…))
5148, 50bitr3id 285 . . . . . . . . . . . . . . . . . . . . . . 23 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ (ran β„Ž = βˆ… ↔ (1...𝑁) = βˆ…))
5251necon3abid 2981 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ (ran β„Ž β‰  βˆ… ↔ Β¬ (1...𝑁) = βˆ…))
5352biimpar 479 . . . . . . . . . . . . . . . . . . . . 21 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ Β¬ (1...𝑁) = βˆ…) β†’ ran β„Ž β‰  βˆ…)
54 rpssre 12929 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ+ βŠ† ℝ
5540, 54sstrdi 3961 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ ran β„Ž βŠ† ℝ)
5655adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ Β¬ (1...𝑁) = βˆ…) β†’ ran β„Ž βŠ† ℝ)
57 ltso 11242 . . . . . . . . . . . . . . . . . . . . . 22 < Or ℝ
58 fiinfcl 9444 . . . . . . . . . . . . . . . . . . . . . 22 (( < Or ℝ ∧ (ran β„Ž ∈ Fin ∧ ran β„Ž β‰  βˆ… ∧ ran β„Ž βŠ† ℝ)) β†’ inf(ran β„Ž, ℝ, < ) ∈ ran β„Ž)
5957, 58mpan 689 . . . . . . . . . . . . . . . . . . . . 21 ((ran β„Ž ∈ Fin ∧ ran β„Ž β‰  βˆ… ∧ ran β„Ž βŠ† ℝ) β†’ inf(ran β„Ž, ℝ, < ) ∈ ran β„Ž)
6047, 53, 56, 59syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ Β¬ (1...𝑁) = βˆ…) β†’ inf(ran β„Ž, ℝ, < ) ∈ ran β„Ž)
6141, 60sseldd 3950 . . . . . . . . . . . . . . . . . . 19 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ Β¬ (1...𝑁) = βˆ…) β†’ inf(ran β„Ž, ℝ, < ) ∈ ℝ+)
6239, 61ifclda 4526 . . . . . . . . . . . . . . . . . 18 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ+)
6362adantr 482 . . . . . . . . . . . . . . . . 17 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›))) β†’ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ+)
6462adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ+)
6564rpxrd 12965 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ*)
66 ffvelcdm 7037 . . . . . . . . . . . . . . . . . . . . . . . 24 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„Žβ€˜π‘›) ∈ ℝ+)
6766rpxrd 12965 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„Žβ€˜π‘›) ∈ ℝ*)
68 ne0i 4299 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ (1...𝑁) β†’ (1...𝑁) β‰  βˆ…)
69 ifnefalse 4503 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1...𝑁) β‰  βˆ… β†’ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) = inf(ran β„Ž, ℝ, < ))
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (1...𝑁) β†’ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) = inf(ran β„Ž, ℝ, < ))
7170adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) = inf(ran β„Ž, ℝ, < ))
7255adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ ran β„Ž βŠ† ℝ)
73 0re 11164 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ ℝ
74 rpge0 12935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℝ+ β†’ 0 ≀ 𝑦)
7574rgen 3067 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 βˆ€π‘¦ ∈ ℝ+ 0 ≀ 𝑦
76 ssralv 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ran β„Ž βŠ† ℝ+ β†’ (βˆ€π‘¦ ∈ ℝ+ 0 ≀ 𝑦 β†’ βˆ€π‘¦ ∈ ran β„Ž0 ≀ 𝑦))
7740, 75, 76mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ βˆ€π‘¦ ∈ ran β„Ž0 ≀ 𝑦)
78 breq1 5113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ = 0 β†’ (π‘₯ ≀ 𝑦 ↔ 0 ≀ 𝑦))
7978ralbidv 3175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ = 0 β†’ (βˆ€π‘¦ ∈ ran β„Ž π‘₯ ≀ 𝑦 ↔ βˆ€π‘¦ ∈ ran β„Ž0 ≀ 𝑦))
8079rspcev 3584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 ∈ ℝ ∧ βˆ€π‘¦ ∈ ran β„Ž0 ≀ 𝑦) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ ran β„Ž π‘₯ ≀ 𝑦)
8173, 77, 80sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ ran β„Ž π‘₯ ≀ 𝑦)
8281adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ ran β„Ž π‘₯ ≀ 𝑦)
83 fnfvelrn 7036 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((β„Ž Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„Žβ€˜π‘›) ∈ ran β„Ž)
8442, 83sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ (β„Žβ€˜π‘›) ∈ ran β„Ž)
85 infrelb 12147 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ran β„Ž βŠ† ℝ ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ ran β„Ž π‘₯ ≀ 𝑦 ∧ (β„Žβ€˜π‘›) ∈ ran β„Ž) β†’ inf(ran β„Ž, ℝ, < ) ≀ (β„Žβ€˜π‘›))
8672, 82, 84, 85syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ inf(ran β„Ž, ℝ, < ) ≀ (β„Žβ€˜π‘›))
8771, 86eqbrtrd 5132 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ≀ (β„Žβ€˜π‘›))
8865, 67, 87jca31 516 . . . . . . . . . . . . . . . . . . . . . 22 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ* ∧ (β„Žβ€˜π‘›) ∈ ℝ*) ∧ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ≀ (β„Žβ€˜π‘›)))
89 ssbl 23792 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐷 ∈ (∞Metβ€˜β„) ∧ (π‘ƒβ€˜π‘›) ∈ ℝ) ∧ (if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ* ∧ (β„Žβ€˜π‘›) ∈ ℝ*) ∧ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ≀ (β„Žβ€˜π‘›)) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)))
90893expb 1121 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐷 ∈ (∞Metβ€˜β„) ∧ (π‘ƒβ€˜π‘›) ∈ ℝ) ∧ ((if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ* ∧ (β„Žβ€˜π‘›) ∈ ℝ*) ∧ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ≀ (β„Žβ€˜π‘›))) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)))
9125, 90mpanl1 699 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ* ∧ (β„Žβ€˜π‘›) ∈ ℝ*) ∧ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ≀ (β„Žβ€˜π‘›))) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)))
9291ancoms 460 . . . . . . . . . . . . . . . . . . . . . 22 ((((if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ* ∧ (β„Žβ€˜π‘›) ∈ ℝ*) ∧ if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ≀ (β„Žβ€˜π‘›)) ∧ (π‘ƒβ€˜π‘›) ∈ ℝ) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)))
9388, 92sylan 581 . . . . . . . . . . . . . . . . . . . . 21 (((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) ∧ (π‘ƒβ€˜π‘›) ∈ ℝ) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)))
94 sstr2 3956 . . . . . . . . . . . . . . . . . . . . 21 (((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) β†’ (((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)))
9593, 94syl 17 . . . . . . . . . . . . . . . . . . . 20 (((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) ∧ (π‘ƒβ€˜π‘›) ∈ ℝ) β†’ (((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)))
9695expimpd 455 . . . . . . . . . . . . . . . . . . 19 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›)) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)))
9796ralimdva 3165 . . . . . . . . . . . . . . . . . 18 (β„Ž:(1...𝑁)βŸΆβ„+ β†’ (βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›)) β†’ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)))
9897imp 408 . . . . . . . . . . . . . . . . 17 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›))) β†’ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›))
9924fveq2i 6850 . . . . . . . . . . . . . . . . . . . . . 22 (ballβ€˜π·) = (ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))
10099oveqi 7375 . . . . . . . . . . . . . . . . . . . . 21 ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) = ((π‘ƒβ€˜π‘›)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )))
101100sseq1i 3977 . . . . . . . . . . . . . . . . . . . 20 (((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›) ↔ ((π‘ƒβ€˜π‘›)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›))
102101ralbii 3097 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›) ↔ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›))
103 nfv 1918 . . . . . . . . . . . . . . . . . . 19 β„²π‘‘βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)
104102, 103nfxfr 1856 . . . . . . . . . . . . . . . . . 18 β„²π‘‘βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)
105 oveq2 7370 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) β†’ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) = ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))))
106105sseq1d 3980 . . . . . . . . . . . . . . . . . . 19 (𝑑 = if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) β†’ (((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›) ↔ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)))
107106ralbidv 3175 . . . . . . . . . . . . . . . . . 18 (𝑑 = if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) β†’ (βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›) ↔ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)))
108104, 107rspce 3573 . . . . . . . . . . . . . . . . 17 ((if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < )) ∈ ℝ+ ∧ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)if((1...𝑁) = βˆ…, 1, inf(ran β„Ž, ℝ, < ))) βŠ† (π‘”β€˜π‘›)) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›))
10963, 98, 108syl2anc 585 . . . . . . . . . . . . . . . 16 ((β„Ž:(1...𝑁)βŸΆβ„+ ∧ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›))) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›))
110109exlimiv 1934 . . . . . . . . . . . . . . 15 (βˆƒβ„Ž(β„Ž:(1...𝑁)βŸΆβ„+ ∧ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›) ∈ ℝ ∧ ((π‘ƒβ€˜π‘›)(ballβ€˜π·)(β„Žβ€˜π‘›)) βŠ† (π‘”β€˜π‘›))) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›))
11137, 110syl 17 . . . . . . . . . . . . . 14 (βˆ€π‘› ∈ (1...𝑁)((π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ (π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›))
11219, 111sylbir 234 . . . . . . . . . . . . 13 ((βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ βˆ€π‘› ∈ (1...𝑁)(π‘ƒβ€˜π‘›) ∈ (π‘”β€˜π‘›)) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›))
11318, 112sylan2 594 . . . . . . . . . . . 12 ((βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (topGenβ€˜ran (,)) ∧ 𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›)) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›))
11416, 113sylanb 582 . . . . . . . . . . 11 ((βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ 𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›)) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›))
115 sstr2 3956 . . . . . . . . . . . . 13 (X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) β†’ (X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) βŠ† 𝑆 β†’ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆))
116 ss2ixp 8855 . . . . . . . . . . . . 13 (βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›) β†’ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›))
117115, 116syl11 33 . . . . . . . . . . . 12 (X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) βŠ† 𝑆 β†’ (βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›) β†’ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆))
118117reximdv 3168 . . . . . . . . . . 11 (X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) βŠ† 𝑆 β†’ (βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘› ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† (π‘”β€˜π‘›) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆))
119114, 118syl5com 31 . . . . . . . . . 10 ((βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ 𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›)) β†’ (X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) βŠ† 𝑆 β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆))
120119expimpd 455 . . . . . . . . 9 (βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†’ ((𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) ∧ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆))
121 eleq2 2827 . . . . . . . . . . 11 (𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) β†’ (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›)))
122 sseq1 3974 . . . . . . . . . . 11 (𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) β†’ (𝑧 βŠ† 𝑆 ↔ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) βŠ† 𝑆))
123121, 122anbi12d 632 . . . . . . . . . 10 (𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) β†’ ((𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆) ↔ (𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) ∧ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) βŠ† 𝑆)))
124123imbi1d 342 . . . . . . . . 9 (𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) β†’ (((𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆) ↔ ((𝑃 ∈ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) ∧ X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆)))
125120, 124syl5ibrcom 247 . . . . . . . 8 (βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†’ (𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) β†’ ((𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆)))
1261253ad2ant2 1135 . . . . . . 7 ((𝑔 Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑧)(π‘”β€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) β†’ (𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›) β†’ ((𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆)))
127126imp 408 . . . . . 6 (((𝑔 Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑧)(π‘”β€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ 𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›)) β†’ ((𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆))
128127exlimiv 1934 . . . . 5 (βˆƒπ‘”((𝑔 Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(π‘”β€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑧)(π‘”β€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ 𝑧 = X𝑛 ∈ (1...𝑁)(π‘”β€˜π‘›)) β†’ ((𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆))
12912, 128sylbi 216 . . . 4 (𝑧 ∈ {π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))} β†’ ((𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆))
130129rexlimiv 3146 . . 3 (βˆƒπ‘§ ∈ {π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))} (𝑃 ∈ 𝑧 ∧ 𝑧 βŠ† 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆)
13111, 130syl 17 . 2 ((𝑆 ∈ (topGenβ€˜{π‘₯ ∣ βˆƒβ„Ž((β„Ž Fn (1...𝑁) ∧ βˆ€π‘› ∈ (1...𝑁)(β„Žβ€˜π‘›) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ ((1...𝑁) βˆ– 𝑀)(β„Žβ€˜π‘›) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›)) ∧ π‘₯ = X𝑛 ∈ (1...𝑁)(β„Žβ€˜π‘›))}) ∧ 𝑃 ∈ 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆)
13210, 131sylanb 582 1 ((𝑆 ∈ 𝑅 ∧ 𝑃 ∈ 𝑆) β†’ βˆƒπ‘‘ ∈ ℝ+ X𝑛 ∈ (1...𝑁)((π‘ƒβ€˜π‘›)(ballβ€˜π·)𝑑) βŠ† 𝑆)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2714   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448   βˆ– cdif 3912   βŠ† wss 3915  βˆ…c0 4287  ifcif 4491  {csn 4591  βˆͺ cuni 4870   class class class wbr 5110   Or wor 5549   Γ— cxp 5636  dom cdm 5638  ran crn 5639   β†Ύ cres 5640   ∘ ccom 5642   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  Xcixp 8842  Fincfn 8890  infcinf 9384  β„cr 11057  0cc0 11058  1c1 11059  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  β„+crp 12922  (,)cioo 13271  ...cfz 13431  abscabs 15126  topGenctg 17326  βˆtcpt 17327  βˆžMetcxmet 20797  ballcbl 20799  MetOpencmopn 20802  Topctop 22258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-fz 13432  df-seq 13914  df-exp 13975  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-topgen 17332  df-pt 17333  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-top 22259  df-topon 22276  df-bases 22312
This theorem is referenced by:  poimirlem29  36136
  Copyright terms: Public domain W3C validator