MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lebnumlem3 Structured version   Visualization version   GIF version

Theorem lebnumlem3 24811
Description: Lemma for lebnum 24812. By the previous lemmas, 𝐹 is continuous and positive on a compact set, so it has a positive minimum π‘Ÿ. Then setting 𝑑 = π‘Ÿ / β™―(π‘ˆ), since for each 𝑒 ∈ π‘ˆ we have ball(π‘₯, 𝑑) βŠ† 𝑒 iff 𝑑 ≀ 𝑑(π‘₯, 𝑋 βˆ– 𝑒), if Β¬ ball(π‘₯, 𝑑) βŠ† 𝑒 for all 𝑒 then summing over 𝑒 yields Σ𝑒 ∈ π‘ˆπ‘‘(π‘₯, 𝑋 βˆ– 𝑒) = 𝐹(π‘₯) < Σ𝑒 ∈ π‘ˆπ‘‘ = π‘Ÿ, in contradiction to the assumption that π‘Ÿ is the minimum of 𝐹. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) (Revised by AV, 30-Sep-2020.)
Hypotheses
Ref Expression
lebnum.j 𝐽 = (MetOpenβ€˜π·)
lebnum.d (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
lebnum.c (πœ‘ β†’ 𝐽 ∈ Comp)
lebnum.s (πœ‘ β†’ π‘ˆ βŠ† 𝐽)
lebnum.u (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
lebnumlem1.u (πœ‘ β†’ π‘ˆ ∈ Fin)
lebnumlem1.n (πœ‘ β†’ Β¬ 𝑋 ∈ π‘ˆ)
lebnumlem1.f 𝐹 = (𝑦 ∈ 𝑋 ↦ Ξ£π‘˜ ∈ π‘ˆ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))
lebnumlem2.k 𝐾 = (topGenβ€˜ran (,))
Assertion
Ref Expression
lebnumlem3 (πœ‘ β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒)
Distinct variable groups:   π‘˜,𝑑,𝑒,π‘₯,𝑦,𝑧,𝐷   𝐽,𝑑,π‘˜,π‘₯,𝑦,𝑧   π‘ˆ,𝑑,π‘˜,𝑒,π‘₯,𝑦,𝑧   π‘₯,𝐹   πœ‘,𝑑,π‘˜,π‘₯,𝑦,𝑧   𝑋,𝑑,π‘˜,𝑒,π‘₯,𝑦,𝑧   π‘₯,𝐾
Allowed substitution hints:   πœ‘(𝑒)   𝐹(𝑦,𝑧,𝑒,π‘˜,𝑑)   𝐽(𝑒)   𝐾(𝑦,𝑧,𝑒,π‘˜,𝑑)

Proof of Theorem lebnumlem3
Dummy variables π‘Ÿ 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1rp 12975 . . . 4 1 ∈ ℝ+
21ne0ii 4329 . . 3 ℝ+ β‰  βˆ…
3 ral0 4504 . . . . 5 βˆ€π‘₯ ∈ βˆ… βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒
4 simpr 484 . . . . . 6 ((πœ‘ ∧ 𝑋 = βˆ…) β†’ 𝑋 = βˆ…)
54raleqdv 3317 . . . . 5 ((πœ‘ ∧ 𝑋 = βˆ…) β†’ (βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒 ↔ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒))
63, 5mpbiri 258 . . . 4 ((πœ‘ ∧ 𝑋 = βˆ…) β†’ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒)
76ralrimivw 3142 . . 3 ((πœ‘ ∧ 𝑋 = βˆ…) β†’ βˆ€π‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒)
8 r19.2z 4486 . . 3 ((ℝ+ β‰  βˆ… ∧ βˆ€π‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒)
92, 7, 8sylancr 586 . 2 ((πœ‘ ∧ 𝑋 = βˆ…) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒)
10 lebnum.j . . . . . . 7 𝐽 = (MetOpenβ€˜π·)
11 lebnum.d . . . . . . 7 (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
12 lebnum.c . . . . . . 7 (πœ‘ β†’ 𝐽 ∈ Comp)
13 lebnum.s . . . . . . 7 (πœ‘ β†’ π‘ˆ βŠ† 𝐽)
14 lebnum.u . . . . . . 7 (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
15 lebnumlem1.u . . . . . . 7 (πœ‘ β†’ π‘ˆ ∈ Fin)
16 lebnumlem1.n . . . . . . 7 (πœ‘ β†’ Β¬ 𝑋 ∈ π‘ˆ)
17 lebnumlem1.f . . . . . . 7 𝐹 = (𝑦 ∈ 𝑋 ↦ Ξ£π‘˜ ∈ π‘ˆ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))
1810, 11, 12, 13, 14, 15, 16, 17lebnumlem1 24809 . . . . . 6 (πœ‘ β†’ 𝐹:π‘‹βŸΆβ„+)
1918adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ 𝐹:π‘‹βŸΆβ„+)
2019frnd 6715 . . . 4 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ ran 𝐹 βŠ† ℝ+)
21 eqid 2724 . . . . . . 7 βˆͺ 𝐽 = βˆͺ 𝐽
22 lebnumlem2.k . . . . . . 7 𝐾 = (topGenβ€˜ran (,))
2312adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ 𝐽 ∈ Comp)
2410, 11, 12, 13, 14, 15, 16, 17, 22lebnumlem2 24810 . . . . . . . 8 (πœ‘ β†’ 𝐹 ∈ (𝐽 Cn 𝐾))
2524adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ 𝐹 ∈ (𝐽 Cn 𝐾))
26 metxmet 24162 . . . . . . . . . 10 (𝐷 ∈ (Metβ€˜π‘‹) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
2710mopnuni 24269 . . . . . . . . . 10 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
2811, 26, 273syl 18 . . . . . . . . 9 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
2928neeq1d 2992 . . . . . . . 8 (πœ‘ β†’ (𝑋 β‰  βˆ… ↔ βˆͺ 𝐽 β‰  βˆ…))
3029biimpa 476 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ βˆͺ 𝐽 β‰  βˆ…)
3121, 22, 23, 25, 30evth2 24808 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ βˆƒπ‘€ ∈ βˆͺ π½βˆ€π‘₯ ∈ βˆͺ 𝐽(πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯))
3228adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ 𝑋 = βˆͺ 𝐽)
33 raleq 3314 . . . . . . . 8 (𝑋 = βˆͺ 𝐽 β†’ (βˆ€π‘₯ ∈ 𝑋 (πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯) ↔ βˆ€π‘₯ ∈ βˆͺ 𝐽(πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯)))
3433rexeqbi1dv 3326 . . . . . . 7 (𝑋 = βˆͺ 𝐽 β†’ (βˆƒπ‘€ ∈ 𝑋 βˆ€π‘₯ ∈ 𝑋 (πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯) ↔ βˆƒπ‘€ ∈ βˆͺ π½βˆ€π‘₯ ∈ βˆͺ 𝐽(πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯)))
3532, 34syl 17 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ (βˆƒπ‘€ ∈ 𝑋 βˆ€π‘₯ ∈ 𝑋 (πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯) ↔ βˆƒπ‘€ ∈ βˆͺ π½βˆ€π‘₯ ∈ βˆͺ 𝐽(πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯)))
3631, 35mpbird 257 . . . . 5 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ βˆƒπ‘€ ∈ 𝑋 βˆ€π‘₯ ∈ 𝑋 (πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯))
37 ffn 6707 . . . . . 6 (𝐹:π‘‹βŸΆβ„+ β†’ 𝐹 Fn 𝑋)
38 breq1 5141 . . . . . . . 8 (π‘Ÿ = (πΉβ€˜π‘€) β†’ (π‘Ÿ ≀ (πΉβ€˜π‘₯) ↔ (πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯)))
3938ralbidv 3169 . . . . . . 7 (π‘Ÿ = (πΉβ€˜π‘€) β†’ (βˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯) ↔ βˆ€π‘₯ ∈ 𝑋 (πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯)))
4039rexrn 7078 . . . . . 6 (𝐹 Fn 𝑋 β†’ (βˆƒπ‘Ÿ ∈ ran πΉβˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯) ↔ βˆƒπ‘€ ∈ 𝑋 βˆ€π‘₯ ∈ 𝑋 (πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯)))
4119, 37, 403syl 18 . . . . 5 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ (βˆƒπ‘Ÿ ∈ ran πΉβˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯) ↔ βˆƒπ‘€ ∈ 𝑋 βˆ€π‘₯ ∈ 𝑋 (πΉβ€˜π‘€) ≀ (πΉβ€˜π‘₯)))
4236, 41mpbird 257 . . . 4 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ βˆƒπ‘Ÿ ∈ ran πΉβˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯))
43 ssrexv 4043 . . . 4 (ran 𝐹 βŠ† ℝ+ β†’ (βˆƒπ‘Ÿ ∈ ran πΉβˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯) β†’ βˆƒπ‘Ÿ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯)))
4420, 42, 43sylc 65 . . 3 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ βˆƒπ‘Ÿ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯))
45 simpr 484 . . . . . 6 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ π‘Ÿ ∈ ℝ+)
4614ad2antrr 723 . . . . . . . . . 10 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑋 = βˆͺ π‘ˆ)
47 simplr 766 . . . . . . . . . 10 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑋 β‰  βˆ…)
4846, 47eqnetrrd 3001 . . . . . . . . 9 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆͺ π‘ˆ β‰  βˆ…)
49 unieq 4910 . . . . . . . . . . 11 (π‘ˆ = βˆ… β†’ βˆͺ π‘ˆ = βˆͺ βˆ…)
50 uni0 4929 . . . . . . . . . . 11 βˆͺ βˆ… = βˆ…
5149, 50eqtrdi 2780 . . . . . . . . . 10 (π‘ˆ = βˆ… β†’ βˆͺ π‘ˆ = βˆ…)
5251necon3i 2965 . . . . . . . . 9 (βˆͺ π‘ˆ β‰  βˆ… β†’ π‘ˆ β‰  βˆ…)
5348, 52syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ π‘ˆ β‰  βˆ…)
5415ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ π‘ˆ ∈ Fin)
55 hashnncl 14323 . . . . . . . . 9 (π‘ˆ ∈ Fin β†’ ((β™―β€˜π‘ˆ) ∈ β„• ↔ π‘ˆ β‰  βˆ…))
5654, 55syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ ((β™―β€˜π‘ˆ) ∈ β„• ↔ π‘ˆ β‰  βˆ…))
5753, 56mpbird 257 . . . . . . 7 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ (β™―β€˜π‘ˆ) ∈ β„•)
5857nnrpd 13011 . . . . . 6 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ (β™―β€˜π‘ˆ) ∈ ℝ+)
5945, 58rpdivcld 13030 . . . . 5 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ ℝ+)
60 ralnex 3064 . . . . . . . 8 (βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒 ↔ Β¬ βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)
6154adantr 480 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ π‘ˆ ∈ Fin)
6253adantr 480 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ π‘ˆ β‰  βˆ…)
63 simprl 768 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ π‘₯ ∈ 𝑋)
6463adantr 480 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ π‘₯ ∈ 𝑋)
65 eqid 2724 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < )) = (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))
6665metdsval 24685 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝑋 β†’ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯) = inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ))
6764, 66syl 17 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯) = inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ))
6811ad2antrr 723 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
6968ad2antrr 723 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
70 difssd 4124 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (𝑋 βˆ– π‘˜) βŠ† 𝑋)
71 elssuni 4931 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ π‘ˆ β†’ π‘˜ βŠ† βˆͺ π‘ˆ)
7271adantl 481 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ π‘˜ βŠ† βˆͺ π‘ˆ)
7346ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ 𝑋 = βˆͺ π‘ˆ)
7472, 73sseqtrrd 4015 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ π‘˜ βŠ† 𝑋)
75 eleq1 2813 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ = 𝑋 β†’ (π‘˜ ∈ π‘ˆ ↔ 𝑋 ∈ π‘ˆ))
7675notbid 318 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑋 β†’ (Β¬ π‘˜ ∈ π‘ˆ ↔ Β¬ 𝑋 ∈ π‘ˆ))
7716, 76syl5ibrcom 246 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘˜ = 𝑋 β†’ Β¬ π‘˜ ∈ π‘ˆ))
7877necon2ad 2947 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π‘˜ ∈ π‘ˆ β†’ π‘˜ β‰  𝑋))
7978ad3antrrr 727 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (π‘˜ ∈ π‘ˆ β†’ π‘˜ β‰  𝑋))
8079imp 406 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ π‘˜ β‰  𝑋)
81 pssdifn0 4357 . . . . . . . . . . . . . . . 16 ((π‘˜ βŠ† 𝑋 ∧ π‘˜ β‰  𝑋) β†’ (𝑋 βˆ– π‘˜) β‰  βˆ…)
8274, 80, 81syl2anc 583 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (𝑋 βˆ– π‘˜) β‰  βˆ…)
8365metdsre 24691 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (𝑋 βˆ– π‘˜) βŠ† 𝑋 ∧ (𝑋 βˆ– π‘˜) β‰  βˆ…) β†’ (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < )):π‘‹βŸΆβ„)
8469, 70, 82, 83syl3anc 1368 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < )):π‘‹βŸΆβ„)
8584, 64ffvelcdmd 7077 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯) ∈ ℝ)
8667, 85eqeltrrd 2826 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ) ∈ ℝ)
8759ad2antrr 723 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ ℝ+)
8887rpred 13013 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ ℝ)
89 simprr 770 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)
90 sseq2 4000 . . . . . . . . . . . . . . . . . 18 (𝑒 = π‘˜ β†’ ((π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒 ↔ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† π‘˜))
9190notbid 318 . . . . . . . . . . . . . . . . 17 (𝑒 = π‘˜ β†’ (Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒 ↔ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† π‘˜))
9291rspccva 3603 . . . . . . . . . . . . . . . 16 ((βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒 ∧ π‘˜ ∈ π‘ˆ) β†’ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† π‘˜)
9389, 92sylan 579 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† π‘˜)
9469, 26syl 17 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
9587rpxrd 13014 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ ℝ*)
9665metdsge 24687 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (𝑋 βˆ– π‘˜) βŠ† 𝑋 ∧ π‘₯ ∈ 𝑋) ∧ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ ℝ*) β†’ ((π‘Ÿ / (β™―β€˜π‘ˆ)) ≀ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯) ↔ ((𝑋 βˆ– π‘˜) ∩ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ)))) = βˆ…))
9794, 70, 64, 95, 96syl31anc 1370 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ ((π‘Ÿ / (β™―β€˜π‘ˆ)) ≀ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯) ↔ ((𝑋 βˆ– π‘˜) ∩ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ)))) = βˆ…))
98 blssm 24246 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ π‘₯ ∈ 𝑋 ∧ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ ℝ*) β†’ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑋)
9994, 64, 95, 98syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑋)
100 difin0ss 4360 . . . . . . . . . . . . . . . . 17 (((𝑋 βˆ– π‘˜) ∩ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ)))) = βˆ… β†’ ((π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑋 β†’ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† π‘˜))
10199, 100syl5com 31 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (((𝑋 βˆ– π‘˜) ∩ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ)))) = βˆ… β†’ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† π‘˜))
10297, 101sylbid 239 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ ((π‘Ÿ / (β™―β€˜π‘ˆ)) ≀ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯) β†’ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† π‘˜))
10393, 102mtod 197 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ Β¬ (π‘Ÿ / (β™―β€˜π‘ˆ)) ≀ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯))
10485, 88ltnled 11358 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ (((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯) < (π‘Ÿ / (β™―β€˜π‘ˆ)) ↔ Β¬ (π‘Ÿ / (β™―β€˜π‘ˆ)) ≀ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯)))
105103, 104mpbird 257 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ))β€˜π‘₯) < (π‘Ÿ / (β™―β€˜π‘ˆ)))
10667, 105eqbrtrrd 5162 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) ∧ π‘˜ ∈ π‘ˆ) β†’ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ) < (π‘Ÿ / (β™―β€˜π‘ˆ)))
10761, 62, 86, 88, 106fsumlt 15743 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ Ξ£π‘˜ ∈ π‘ˆ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ) < Ξ£π‘˜ ∈ π‘ˆ (π‘Ÿ / (β™―β€˜π‘ˆ)))
108 oveq1 7408 . . . . . . . . . . . . . . . . 17 (𝑦 = π‘₯ β†’ (𝑦𝐷𝑧) = (π‘₯𝐷𝑧))
109108mpteq2dv 5240 . . . . . . . . . . . . . . . 16 (𝑦 = π‘₯ β†’ (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)) = (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)))
110109rneqd 5927 . . . . . . . . . . . . . . 15 (𝑦 = π‘₯ β†’ ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)) = ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)))
111110infeq1d 9468 . . . . . . . . . . . . . 14 (𝑦 = π‘₯ β†’ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ) = inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ))
112111sumeq2sdv 15647 . . . . . . . . . . . . 13 (𝑦 = π‘₯ β†’ Ξ£π‘˜ ∈ π‘ˆ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (𝑦𝐷𝑧)), ℝ*, < ) = Ξ£π‘˜ ∈ π‘ˆ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ))
113 sumex 15631 . . . . . . . . . . . . 13 Ξ£π‘˜ ∈ π‘ˆ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ) ∈ V
114112, 17, 113fvmpt 6988 . . . . . . . . . . . 12 (π‘₯ ∈ 𝑋 β†’ (πΉβ€˜π‘₯) = Ξ£π‘˜ ∈ π‘ˆ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ))
11563, 114syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (πΉβ€˜π‘₯) = Ξ£π‘˜ ∈ π‘ˆ inf(ran (𝑧 ∈ (𝑋 βˆ– π‘˜) ↦ (π‘₯𝐷𝑧)), ℝ*, < ))
11659adantr 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ ℝ+)
117116rpcnd 13015 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ β„‚)
118 fsumconst 15733 . . . . . . . . . . . . 13 ((π‘ˆ ∈ Fin ∧ (π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ β„‚) β†’ Ξ£π‘˜ ∈ π‘ˆ (π‘Ÿ / (β™―β€˜π‘ˆ)) = ((β™―β€˜π‘ˆ) Β· (π‘Ÿ / (β™―β€˜π‘ˆ))))
11961, 117, 118syl2anc 583 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ Ξ£π‘˜ ∈ π‘ˆ (π‘Ÿ / (β™―β€˜π‘ˆ)) = ((β™―β€˜π‘ˆ) Β· (π‘Ÿ / (β™―β€˜π‘ˆ))))
120 simplr 766 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ π‘Ÿ ∈ ℝ+)
121120rpcnd 13015 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ π‘Ÿ ∈ β„‚)
12257adantr 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (β™―β€˜π‘ˆ) ∈ β„•)
123122nncnd 12225 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (β™―β€˜π‘ˆ) ∈ β„‚)
124122nnne0d 12259 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (β™―β€˜π‘ˆ) β‰  0)
125121, 123, 124divcan2d 11989 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ ((β™―β€˜π‘ˆ) Β· (π‘Ÿ / (β™―β€˜π‘ˆ))) = π‘Ÿ)
126119, 125eqtr2d 2765 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ π‘Ÿ = Ξ£π‘˜ ∈ π‘ˆ (π‘Ÿ / (β™―β€˜π‘ˆ)))
127107, 115, 1263brtr4d 5170 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (πΉβ€˜π‘₯) < π‘Ÿ)
12819ad2antrr 723 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ 𝐹:π‘‹βŸΆβ„+)
129128, 63ffvelcdmd 7077 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (πΉβ€˜π‘₯) ∈ ℝ+)
130129rpred 13013 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
131120rpred 13013 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ π‘Ÿ ∈ ℝ)
132130, 131ltnled 11358 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ ((πΉβ€˜π‘₯) < π‘Ÿ ↔ Β¬ π‘Ÿ ≀ (πΉβ€˜π‘₯)))
133127, 132mpbid 231 . . . . . . . . 9 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒)) β†’ Β¬ π‘Ÿ ≀ (πΉβ€˜π‘₯))
134133expr 456 . . . . . . . 8 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ π‘₯ ∈ 𝑋) β†’ (βˆ€π‘’ ∈ π‘ˆ Β¬ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒 β†’ Β¬ π‘Ÿ ≀ (πΉβ€˜π‘₯)))
13560, 134biimtrrid 242 . . . . . . 7 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ π‘₯ ∈ 𝑋) β†’ (Β¬ βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒 β†’ Β¬ π‘Ÿ ≀ (πΉβ€˜π‘₯)))
136135con4d 115 . . . . . 6 ((((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) ∧ π‘₯ ∈ 𝑋) β†’ (π‘Ÿ ≀ (πΉβ€˜π‘₯) β†’ βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒))
137136ralimdva 3159 . . . . 5 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯) β†’ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒))
138 oveq2 7409 . . . . . . . . 9 (𝑑 = (π‘Ÿ / (β™―β€˜π‘ˆ)) β†’ (π‘₯(ballβ€˜π·)𝑑) = (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))))
139138sseq1d 4005 . . . . . . . 8 (𝑑 = (π‘Ÿ / (β™―β€˜π‘ˆ)) β†’ ((π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒 ↔ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒))
140139rexbidv 3170 . . . . . . 7 (𝑑 = (π‘Ÿ / (β™―β€˜π‘ˆ)) β†’ (βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒 ↔ βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒))
141140ralbidv 3169 . . . . . 6 (𝑑 = (π‘Ÿ / (β™―β€˜π‘ˆ)) β†’ (βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒 ↔ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒))
142141rspcev 3604 . . . . 5 (((π‘Ÿ / (β™―β€˜π‘ˆ)) ∈ ℝ+ ∧ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)(π‘Ÿ / (β™―β€˜π‘ˆ))) βŠ† 𝑒) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒)
14359, 137, 142syl6an 681 . . . 4 (((πœ‘ ∧ 𝑋 β‰  βˆ…) ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒))
144143rexlimdva 3147 . . 3 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 π‘Ÿ ≀ (πΉβ€˜π‘₯) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒))
14544, 144mpd 15 . 2 ((πœ‘ ∧ 𝑋 β‰  βˆ…) β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒)
1469, 145pm2.61dane 3021 1 (πœ‘ β†’ βˆƒπ‘‘ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘’ ∈ π‘ˆ (π‘₯(ballβ€˜π·)𝑑) βŠ† 𝑒)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062   βˆ– cdif 3937   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  βˆͺ cuni 4899   class class class wbr 5138   ↦ cmpt 5221  ran crn 5667   Fn wfn 6528  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401  Fincfn 8935  infcinf 9432  β„‚cc 11104  β„cr 11105  1c1 11107   Β· cmul 11111  β„*cxr 11244   < clt 11245   ≀ cle 11246   / cdiv 11868  β„•cn 12209  β„+crp 12971  (,)cioo 13321  β™―chash 14287  Ξ£csu 15629  topGenctg 17382  βˆžMetcxmet 21213  Metcmet 21214  ballcbl 21215  MetOpencmopn 21218   Cn ccn 23050  Compccmp 23212
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-inf2 9632  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  ax-addf 11185
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-tp 4625  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-se 5622  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-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-ec 8701  df-map 8818  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  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-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-cn 23053  df-cnp 23054  df-cmp 23213  df-tx 23388  df-hmeo 23581  df-xms 24148  df-ms 24149  df-tms 24150
This theorem is referenced by:  lebnum  24812
  Copyright terms: Public domain W3C validator