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 β€˜ 𝐷 ) 𝑑 ) βŠ† 𝑒 )