# 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 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
lebnum.d ${⊢}{\phi }\to {D}\in \mathrm{Met}\left({X}\right)$
lebnum.c ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
lebnum.s ${⊢}{\phi }\to {U}\subseteq {J}$
lebnum.u ${⊢}{\phi }\to {X}=\bigcup {U}$
lebnumlem1.u ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
lebnumlem1.n ${⊢}{\phi }\to ¬{X}\in {U}$
lebnumlem1.f ${⊢}{F}=\left({y}\in {X}⟼\sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)$
lebnumlem2.k ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
Assertion lebnumlem3 ${⊢}{\phi }\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$

### Proof

Step Hyp Ref Expression
1 lebnum.j ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 lebnum.d ${⊢}{\phi }\to {D}\in \mathrm{Met}\left({X}\right)$
3 lebnum.c ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
4 lebnum.s ${⊢}{\phi }\to {U}\subseteq {J}$
5 lebnum.u ${⊢}{\phi }\to {X}=\bigcup {U}$
6 lebnumlem1.u ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
7 lebnumlem1.n ${⊢}{\phi }\to ¬{X}\in {U}$
8 lebnumlem1.f ${⊢}{F}=\left({y}\in {X}⟼\sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)$
9 lebnumlem2.k ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
10 1rp ${⊢}1\in {ℝ}^{+}$
11 10 ne0ii ${⊢}{ℝ}^{+}\ne \varnothing$
12 ral0 ${⊢}\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$
13 simpr ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to {X}=\varnothing$
14 13 raleqdv ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}↔\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}\right)$
15 12 14 mpbiri ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$
16 15 ralrimivw ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$
17 r19.2z ${⊢}\left({ℝ}^{+}\ne \varnothing \wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$
18 11 16 17 sylancr ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$
19 1 2 3 4 5 6 7 8 lebnumlem1 ${⊢}{\phi }\to {F}:{X}⟶{ℝ}^{+}$
20 19 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to {F}:{X}⟶{ℝ}^{+}$
21 20 frnd ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{ran}{F}\subseteq {ℝ}^{+}$
22 eqid ${⊢}\bigcup {J}=\bigcup {J}$
23 3 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to {J}\in \mathrm{Comp}$
24 1 2 3 4 5 6 7 8 9 lebnumlem2 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
25 24 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
26 metxmet ${⊢}{D}\in \mathrm{Met}\left({X}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
27 1 mopnuni ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}=\bigcup {J}$
28 2 26 27 3syl ${⊢}{\phi }\to {X}=\bigcup {J}$
29 28 neeq1d ${⊢}{\phi }\to \left({X}\ne \varnothing ↔\bigcup {J}\ne \varnothing \right)$
30 29 biimpa ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \bigcup {J}\ne \varnothing$
31 22 9 23 25 30 evth2 ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \exists {w}\in \bigcup {J}\phantom{\rule{.4em}{0ex}}\forall {x}\in \bigcup {J}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)$
32 28 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to {X}=\bigcup {J}$
33 raleq ${⊢}{X}=\bigcup {J}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)↔\forall {x}\in \bigcup {J}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)\right)$
34 33 rexeqbi1dv ${⊢}{X}=\bigcup {J}\to \left(\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)↔\exists {w}\in \bigcup {J}\phantom{\rule{.4em}{0ex}}\forall {x}\in \bigcup {J}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)\right)$
35 32 34 syl ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \left(\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)↔\exists {w}\in \bigcup {J}\phantom{\rule{.4em}{0ex}}\forall {x}\in \bigcup {J}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)\right)$
36 31 35 mpbird ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)$
37 ffn ${⊢}{F}:{X}⟶{ℝ}^{+}\to {F}Fn{X}$
38 breq1 ${⊢}{r}={F}\left({w}\right)\to \left({r}\le {F}\left({x}\right)↔{F}\left({w}\right)\le {F}\left({x}\right)\right)$
39 38 ralbidv ${⊢}{r}={F}\left({w}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)\right)$
40 39 rexrn ${⊢}{F}Fn{X}\to \left(\exists {r}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)↔\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)\right)$
41 20 37 40 3syl ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \left(\exists {r}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)↔\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\le {F}\left({x}\right)\right)$
42 36 41 mpbird ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \exists {r}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)$
43 ssrexv ${⊢}\mathrm{ran}{F}\subseteq {ℝ}^{+}\to \left(\exists {r}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)\right)$
44 21 42 43 sylc ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)$
45 simpr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to {r}\in {ℝ}^{+}$
46 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to {X}=\bigcup {U}$
47 simplr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to {X}\ne \varnothing$
48 46 47 eqnetrrd ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to \bigcup {U}\ne \varnothing$
49 unieq ${⊢}{U}=\varnothing \to \bigcup {U}=\bigcup \varnothing$
50 uni0 ${⊢}\bigcup \varnothing =\varnothing$
51 49 50 eqtrdi ${⊢}{U}=\varnothing \to \bigcup {U}=\varnothing$
52 51 necon3i ${⊢}\bigcup {U}\ne \varnothing \to {U}\ne \varnothing$
53 48 52 syl ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to {U}\ne \varnothing$
54 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to {U}\in \mathrm{Fin}$
55 hashnncl ${⊢}{U}\in \mathrm{Fin}\to \left(\left|{U}\right|\in ℕ↔{U}\ne \varnothing \right)$
56 54 55 syl ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to \left(\left|{U}\right|\in ℕ↔{U}\ne \varnothing \right)$
57 53 56 mpbird ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to \left|{U}\right|\in ℕ$
58 57 nnrpd ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to \left|{U}\right|\in {ℝ}^{+}$
59 45 58 rpdivcld ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to \frac{{r}}{\left|{U}\right|}\in {ℝ}^{+}$
60 ralnex ${⊢}\forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}↔¬\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}$
61 54 adantr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {U}\in \mathrm{Fin}$
62 53 adantr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {U}\ne \varnothing$
63 simprl ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {x}\in {X}$
64 63 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {x}\in {X}$
65 eqid ${⊢}\left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)=\left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)$
66 65 metdsval ${⊢}{x}\in {X}\to \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)=sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)$
67 64 66 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)=sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)$
68 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to {D}\in \mathrm{Met}\left({X}\right)$
69 68 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {D}\in \mathrm{Met}\left({X}\right)$
70 difssd ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {X}\setminus {k}\subseteq {X}$
71 elssuni ${⊢}{k}\in {U}\to {k}\subseteq \bigcup {U}$
72 71 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {k}\subseteq \bigcup {U}$
73 46 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {X}=\bigcup {U}$
74 72 73 sseqtrrd ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {k}\subseteq {X}$
75 eleq1 ${⊢}{k}={X}\to \left({k}\in {U}↔{X}\in {U}\right)$
76 75 notbid ${⊢}{k}={X}\to \left(¬{k}\in {U}↔¬{X}\in {U}\right)$
77 7 76 syl5ibrcom ${⊢}{\phi }\to \left({k}={X}\to ¬{k}\in {U}\right)$
78 77 necon2ad ${⊢}{\phi }\to \left({k}\in {U}\to {k}\ne {X}\right)$
79 78 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \left({k}\in {U}\to {k}\ne {X}\right)$
80 79 imp ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {k}\ne {X}$
81 pssdifn0 ${⊢}\left({k}\subseteq {X}\wedge {k}\ne {X}\right)\to {X}\setminus {k}\ne \varnothing$
82 74 80 81 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {X}\setminus {k}\ne \varnothing$
83 65 metdsre ${⊢}\left({D}\in \mathrm{Met}\left({X}\right)\wedge {X}\setminus {k}\subseteq {X}\wedge {X}\setminus {k}\ne \varnothing \right)\to \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right):{X}⟶ℝ$
84 69 70 82 83 syl3anc ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right):{X}⟶ℝ$
85 84 64 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)\in ℝ$
86 67 85 eqeltrrd ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ$
87 59 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \frac{{r}}{\left|{U}\right|}\in {ℝ}^{+}$
88 87 rpred ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \frac{{r}}{\left|{U}\right|}\in ℝ$
89 simprr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}$
90 sseq2 ${⊢}{u}={k}\to \left({x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}↔{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {k}\right)$
91 90 notbid ${⊢}{u}={k}\to \left(¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}↔¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {k}\right)$
92 91 rspccva ${⊢}\left(\forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\wedge {k}\in {U}\right)\to ¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {k}$
93 89 92 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to ¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {k}$
94 69 26 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
95 87 rpxrd ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \frac{{r}}{\left|{U}\right|}\in {ℝ}^{*}$
96 65 metdsge ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {X}\setminus {k}\subseteq {X}\wedge {x}\in {X}\right)\wedge \frac{{r}}{\left|{U}\right|}\in {ℝ}^{*}\right)\to \left(\frac{{r}}{\left|{U}\right|}\le \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)↔\left({X}\setminus {k}\right)\cap \left({x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\right)=\varnothing \right)$
97 94 70 64 95 96 syl31anc ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \left(\frac{{r}}{\left|{U}\right|}\le \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)↔\left({X}\setminus {k}\right)\cap \left({x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\right)=\varnothing \right)$
98 blssm ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge \frac{{r}}{\left|{U}\right|}\in {ℝ}^{*}\right)\to {x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {X}$
99 94 64 95 98 syl3anc ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to {x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {X}$
100 difin0ss ${⊢}\left({X}\setminus {k}\right)\cap \left({x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\right)=\varnothing \to \left({x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {X}\to {x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {k}\right)$
101 99 100 syl5com ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \left(\left({X}\setminus {k}\right)\cap \left({x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\right)=\varnothing \to {x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {k}\right)$
102 97 101 sylbid ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \left(\frac{{r}}{\left|{U}\right|}\le \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)\to {x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {k}\right)$
103 93 102 mtod ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to ¬\frac{{r}}{\left|{U}\right|}\le \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)$
104 85 88 ltnled ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \left(\left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)<\frac{{r}}{\left|{U}\right|}↔¬\frac{{r}}{\left|{U}\right|}\le \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)\right)$
105 103 104 mpbird ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to \left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({x}\right)<\frac{{r}}{\left|{U}\right|}$
106 67 105 eqbrtrrd ${⊢}\left(\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\wedge {k}\in {U}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)<\frac{{r}}{\left|{U}\right|}$
107 61 62 86 88 106 fsumlt ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)<\sum _{{k}\in {U}}\left(\frac{{r}}{\left|{U}\right|}\right)$
108 oveq1 ${⊢}{y}={x}\to {y}{D}{z}={x}{D}{z}$
109 108 mpteq2dv ${⊢}{y}={x}\to \left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right)=\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right)$
110 109 rneqd ${⊢}{y}={x}\to \mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right)=\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right)$
111 110 infeq1d ${⊢}{y}={x}\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)$
112 111 sumeq2sdv ${⊢}{y}={x}\to \sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)=\sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)$
113 sumex ${⊢}\sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)\in \mathrm{V}$
114 112 8 113 fvmpt ${⊢}{x}\in {X}\to {F}\left({x}\right)=\sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)$
115 63 114 syl ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {F}\left({x}\right)=\sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{x}{D}{z}\right),{ℝ}^{*},<\right)$
116 59 adantr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \frac{{r}}{\left|{U}\right|}\in {ℝ}^{+}$
117 116 rpcnd ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \frac{{r}}{\left|{U}\right|}\in ℂ$
118 fsumconst ${⊢}\left({U}\in \mathrm{Fin}\wedge \frac{{r}}{\left|{U}\right|}\in ℂ\right)\to \sum _{{k}\in {U}}\left(\frac{{r}}{\left|{U}\right|}\right)=\left|{U}\right|\left(\frac{{r}}{\left|{U}\right|}\right)$
119 61 117 118 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \sum _{{k}\in {U}}\left(\frac{{r}}{\left|{U}\right|}\right)=\left|{U}\right|\left(\frac{{r}}{\left|{U}\right|}\right)$
120 simplr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {r}\in {ℝ}^{+}$
121 120 rpcnd ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {r}\in ℂ$
122 57 adantr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \left|{U}\right|\in ℕ$
123 122 nncnd ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \left|{U}\right|\in ℂ$
124 122 nnne0d ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \left|{U}\right|\ne 0$
125 121 123 124 divcan2d ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \left|{U}\right|\left(\frac{{r}}{\left|{U}\right|}\right)={r}$
126 119 125 eqtr2d ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {r}=\sum _{{k}\in {U}}\left(\frac{{r}}{\left|{U}\right|}\right)$
127 107 115 126 3brtr4d ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {F}\left({x}\right)<{r}$
128 20 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {F}:{X}⟶{ℝ}^{+}$
129 128 63 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {F}\left({x}\right)\in {ℝ}^{+}$
130 129 rpred ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {F}\left({x}\right)\in ℝ$
131 120 rpred ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to {r}\in ℝ$
132 130 131 ltnled ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to \left({F}\left({x}\right)<{r}↔¬{r}\le {F}\left({x}\right)\right)$
133 127 132 mpbid ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge \left({x}\in {X}\wedge \forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\right)\to ¬{r}\le {F}\left({x}\right)$
134 133 expr ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left(\forall {u}\in {U}\phantom{\rule{.4em}{0ex}}¬{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\to ¬{r}\le {F}\left({x}\right)\right)$
135 60 134 syl5bir ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left(¬\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\to ¬{r}\le {F}\left({x}\right)\right)$
136 135 con4d ${⊢}\left(\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\wedge {x}\in {X}\right)\to \left({r}\le {F}\left({x}\right)\to \exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)$
137 136 ralimdva ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)$
138 oveq2 ${⊢}{d}=\frac{{r}}{\left|{U}\right|}\to {x}\mathrm{ball}\left({D}\right){d}={x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)$
139 138 sseq1d ${⊢}{d}=\frac{{r}}{\left|{U}\right|}\to \left({x}\mathrm{ball}\left({D}\right){d}\subseteq {u}↔{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)$
140 139 rexbidv ${⊢}{d}=\frac{{r}}{\left|{U}\right|}\to \left(\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}↔\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)$
141 140 ralbidv ${⊢}{d}=\frac{{r}}{\left|{U}\right|}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)$
142 141 rspcev ${⊢}\left(\frac{{r}}{\left|{U}\right|}\in {ℝ}^{+}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right)\left(\frac{{r}}{\left|{U}\right|}\right)\subseteq {u}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$
143 59 137 142 syl6an ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {r}\in {ℝ}^{+}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}\right)$
144 143 rexlimdva ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{r}\le {F}\left({x}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}\right)$
145 44 144 mpd ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$
146 18 145 pm2.61dane ${⊢}{\phi }\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({D}\right){d}\subseteq {u}$