Metamath Proof Explorer

Theorem lebnumlem3

Description: Lemma for lebnum . By the previous lemmas, F is continuous and positive on a compact set, so it has a positive minimum r . Then setting d = r / # ( U ) , since for each u e. U we have ball ( x , d ) C_ u iff d <_ d ( x , X \ u ) , if -. ball ( x , d ) C_ u for all u then summing over u yields sum_ u e. U d ( x , X \ u ) = F ( x ) < sum_ u e. U d = r , in contradiction to the assumption that r is the minimum of F . (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 5-Sep-2015) (Revised by AV, 30-Sep-2020)

Ref Expression
Hypotheses 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 lebnumlem3 ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )

Proof

Step Hyp Ref Expression
1 lebnum.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 lebnum.d ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 lebnum.c ⊢ ( 𝜑 → 𝐽 ∈ Comp )
4 lebnum.s ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
5 lebnum.u ⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
6 lebnumlem1.u ⊢ ( 𝜑 → 𝑈 ∈ Fin )
7 lebnumlem1.n ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
8 lebnumlem1.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) )
9 lebnumlem2.k ⊢ 𝐾 = ( topGen ‘ ran (,) )
10 1rp ⊢ 1 ∈ ℝ+
11 10 ne0ii ⊢ ℝ+ ≠ ∅
12 ral0 ⊢ ∀ 𝑥 ∈ ∅ ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢
13 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝑋 = ∅ )
14 13 raleqdv ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∀ 𝑥 ∈ ∅ ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
15 12 14 mpbiri ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
16 15 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∀ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
17 r19.2z ⊢ ( ( ℝ+ ≠ ∅ ∧ ∀ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
18 11 16 17 sylancr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
19 1 2 3 4 5 6 7 8 lebnumlem1 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ+ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐹 : 𝑋 ⟶ ℝ+ )
21 20 frnd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ran 𝐹 ⊆ ℝ+ )
22 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
23 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐽 ∈ Comp )
24 1 2 3 4 5 6 7 8 9 lebnumlem2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
26 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
27 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
28 2 26 27 3syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
29 28 neeq1d ⊢ ( 𝜑 → ( 𝑋 ≠ ∅ ↔ ∪ 𝐽 ≠ ∅ ) )
30 29 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∪ 𝐽 ≠ ∅ )
31 22 9 23 25 30 evth2 ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑤 ∈ ∪ 𝐽 ∀ 𝑥 ∈ ∪ 𝐽 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) )
32 28 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 = ∪ 𝐽 )
33 raleq ⊢ ( 𝑋 = ∪ 𝐽 → ( ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ∪ 𝐽 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
34 33 rexeqbi1dv ⊢ ( 𝑋 = ∪ 𝐽 → ( ∃ 𝑤 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑤 ∈ ∪ 𝐽 ∀ 𝑥 ∈ ∪ 𝐽 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
35 32 34 syl ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑤 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑤 ∈ ∪ 𝐽 ∀ 𝑥 ∈ ∪ 𝐽 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
36 31 35 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) )
37 ffn ⊢ ( 𝐹 : 𝑋 ⟶ ℝ+ → 𝐹 Fn 𝑋 )
38 breq1 ⊢ ( 𝑟 = ( 𝐹 ‘ 𝑤 ) → ( 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
39 38 ralbidv ⊢ ( 𝑟 = ( 𝐹 ‘ 𝑤 ) → ( ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
40 39 rexrn ⊢ ( 𝐹 Fn 𝑋 → ( ∃ 𝑟 ∈ ran 𝐹 ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑤 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
41 20 37 40 3syl ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑟 ∈ ran 𝐹 ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑤 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
42 36 41 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑟 ∈ ran 𝐹 ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) )
43 ssrexv ⊢ ( ran 𝐹 ⊆ ℝ+ → ( ∃ 𝑟 ∈ ran 𝐹 ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) ) )
44 21 42 43 sylc ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) )
45 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
46 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑋 = ∪ 𝑈 )
47 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑋 ≠ ∅ )
48 46 47 eqnetrrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → ∪ 𝑈 ≠ ∅ )
49 unieq ⊢ ( 𝑈 = ∅ → ∪ 𝑈 = ∪ ∅ )
50 uni0 ⊢ ∪ ∅ = ∅
51 49 50 eqtrdi ⊢ ( 𝑈 = ∅ → ∪ 𝑈 = ∅ )
52 51 necon3i ⊢ ( ∪ 𝑈 ≠ ∅ → 𝑈 ≠ ∅ )
53 48 52 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑈 ≠ ∅ )
54 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → 𝑈 ∈ Fin )
55 hashnncl ⊢ ( 𝑈 ∈ Fin → ( ( ♯ ‘ 𝑈 ) ∈ ℕ ↔ 𝑈 ≠ ∅ ) )
56 54 55 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → ( ( ♯ ‘ 𝑈 ) ∈ ℕ ↔ 𝑈 ≠ ∅ ) )
57 53 56 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → ( ♯ ‘ 𝑈 ) ∈ ℕ )
58 57 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → ( ♯ ‘ 𝑈 ) ∈ ℝ+ )
59 45 58 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℝ+ )
60 ralnex ⊢ ( ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ↔ ¬ ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 )
61 54 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → 𝑈 ∈ Fin )
62 53 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → 𝑈 ≠ ∅ )
63 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → 𝑥 ∈ 𝑋 )
64 63 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → 𝑥 ∈ 𝑋 )
65 eqid ⊢ ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) = ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) )
66 65 metdsval ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) = inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) )
67 64 66 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) = inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) )
68 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
69 68 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
70 difssd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ∖ 𝑘 ) ⊆ 𝑋 )
71 elssuni ⊢ ( 𝑘 ∈ 𝑈 → 𝑘 ⊆ ∪ 𝑈 )
72 71 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ⊆ ∪ 𝑈 )
73 46 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → 𝑋 = ∪ 𝑈 )
74 72 73 sseqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ⊆ 𝑋 )
75 eleq1 ⊢ ( 𝑘 = 𝑋 → ( 𝑘 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
76 75 notbid ⊢ ( 𝑘 = 𝑋 → ( ¬ 𝑘 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈 ) )
77 7 76 syl5ibrcom ⊢ ( 𝜑 → ( 𝑘 = 𝑋 → ¬ 𝑘 ∈ 𝑈 ) )
78 77 necon2ad ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋 ) )
79 78 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( 𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋 ) )
80 79 imp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ≠ 𝑋 )
81 pssdifn0 ⊢ ( ( 𝑘 ⊆ 𝑋 ∧ 𝑘 ≠ 𝑋 ) → ( 𝑋 ∖ 𝑘 ) ≠ ∅ )
82 74 80 81 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ∖ 𝑘 ) ≠ ∅ )
83 65 metdsre ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑘 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑘 ) ≠ ∅ ) → ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) : 𝑋 ⟶ ℝ )
84 69 70 82 83 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) : 𝑋 ⟶ ℝ )
85 84 64 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) ∈ ℝ )
86 67 85 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) ∈ ℝ )
87 59 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℝ+ )
88 87 rpred ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℝ )
89 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 )
90 sseq2 ⊢ ( 𝑢 = 𝑘 → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ↔ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑘 ) )
91 90 notbid ⊢ ( 𝑢 = 𝑘 → ( ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ↔ ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑘 ) )
92 91 rspccva ⊢ ( ( ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ∧ 𝑘 ∈ 𝑈 ) → ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑘 )
93 89 92 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑘 )
94 69 26 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
95 87 rpxrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℝ* )
96 65 metdsge ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑘 ) ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℝ* ) → ( ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ≤ ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) ↔ ( ( 𝑋 ∖ 𝑘 ) ∩ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ) = ∅ ) )
97 94 70 64 95 96 syl31anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ≤ ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) ↔ ( ( 𝑋 ∖ 𝑘 ) ∩ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ) = ∅ ) )
98 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑋 )
99 94 64 95 98 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑋 )
100 difin0ss ⊢ ( ( ( 𝑋 ∖ 𝑘 ) ∩ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ) = ∅ → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑋 → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑘 ) )
101 99 100 syl5com ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( ( ( 𝑋 ∖ 𝑘 ) ∩ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ) = ∅ → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑘 ) )
102 97 101 sylbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ≤ ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑘 ) )
103 93 102 mtod ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ¬ ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ≤ ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) )
104 85 88 ltnled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) < ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ↔ ¬ ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ≤ ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) ) )
105 103 104 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ‘ 𝑥 ) < ( 𝑟 / ( ♯ ‘ 𝑈 ) ) )
106 67 105 eqbrtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ 𝑈 ) → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) < ( 𝑟 / ( ♯ ‘ 𝑈 ) ) )
107 61 62 86 88 106 fsumlt ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) < Σ 𝑘 ∈ 𝑈 ( 𝑟 / ( ♯ ‘ 𝑈 ) ) )
108 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝐷 𝑧 ) = ( 𝑥 𝐷 𝑧 ) )
109 108 mpteq2dv ⊢ ( 𝑦 = 𝑥 → ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) = ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) )
110 109 rneqd ⊢ ( 𝑦 = 𝑥 → ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) = ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) )
111 110 infeq1d ⊢ ( 𝑦 = 𝑥 → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) = inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) )
112 111 sumeq2sdv ⊢ ( 𝑦 = 𝑥 → Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) = Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) )
113 sumex ⊢ Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) ∈ V
114 112 8 113 fvmpt ⊢ ( 𝑥 ∈ 𝑋 → ( 𝐹 ‘ 𝑥 ) = Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) )
115 63 114 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( 𝐹 ‘ 𝑥 ) = Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑥 𝐷 𝑧 ) ) , ℝ* , < ) )
116 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℝ+ )
117 116 rpcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℂ )
118 fsumconst ⊢ ( ( 𝑈 ∈ Fin ∧ ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℂ ) → Σ 𝑘 ∈ 𝑈 ( 𝑟 / ( ♯ ‘ 𝑈 ) ) = ( ( ♯ ‘ 𝑈 ) · ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) )
119 61 117 118 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → Σ 𝑘 ∈ 𝑈 ( 𝑟 / ( ♯ ‘ 𝑈 ) ) = ( ( ♯ ‘ 𝑈 ) · ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) )
120 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → 𝑟 ∈ ℝ+ )
121 120 rpcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → 𝑟 ∈ ℂ )
122 57 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( ♯ ‘ 𝑈 ) ∈ ℕ )
123 122 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( ♯ ‘ 𝑈 ) ∈ ℂ )
124 122 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( ♯ ‘ 𝑈 ) ≠ 0 )
125 121 123 124 divcan2d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( ( ♯ ‘ 𝑈 ) · ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) = 𝑟 )
126 119 125 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → 𝑟 = Σ 𝑘 ∈ 𝑈 ( 𝑟 / ( ♯ ‘ 𝑈 ) ) )
127 107 115 126 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( 𝐹 ‘ 𝑥 ) < 𝑟 )
128 20 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → 𝐹 : 𝑋 ⟶ ℝ+ )
129 128 63 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ+ )
130 129 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
131 120 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → 𝑟 ∈ ℝ )
132 130 131 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ( ( 𝐹 ‘ 𝑥 ) < 𝑟 ↔ ¬ 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) ) )
133 127 132 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) ) → ¬ 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) )
134 133 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑢 ∈ 𝑈 ¬ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 → ¬ 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) ) )
135 60 134 biimtrrid ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ¬ ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 → ¬ 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) ) )
136 135 con4d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) )
137 136 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) )
138 oveq2 ⊢ ( 𝑑 = ( 𝑟 / ( ♯ ‘ 𝑈 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) = ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) )
139 138 sseq1d ⊢ ( 𝑑 = ( 𝑟 / ( ♯ ‘ 𝑈 ) ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) )
140 139 rexbidv ⊢ ( 𝑑 = ( 𝑟 / ( ♯ ‘ 𝑈 ) ) → ( ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) )
141 140 ralbidv ⊢ ( 𝑑 = ( 𝑟 / ( ♯ ‘ 𝑈 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) )
142 141 rspcev ⊢ ( ( ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ∈ ℝ+ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / ( ♯ ‘ 𝑈 ) ) ) ⊆ 𝑢 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
143 59 137 142 syl6an ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
144 143 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 𝑟 ≤ ( 𝐹 ‘ 𝑥 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
145 44 144 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
146 18 145 pm2.61dane ⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )