Metamath Proof Explorer

Theorem lebnumlem1

Description: Lemma for lebnum . The function F measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-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)$
Assertion lebnumlem1 ${⊢}{\phi }\to {F}:{X}⟶{ℝ}^{+}$

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 6 adantr ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {U}\in \mathrm{Fin}$
10 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {D}\in \mathrm{Met}\left({X}\right)$
11 difssd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {X}\setminus {k}\subseteq {X}$
12 4 adantr ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {U}\subseteq {J}$
13 12 sselda ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {k}\in {J}$
14 elssuni ${⊢}{k}\in {J}\to {k}\subseteq \bigcup {J}$
15 13 14 syl ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {k}\subseteq \bigcup {J}$
16 metxmet ${⊢}{D}\in \mathrm{Met}\left({X}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
17 2 16 syl ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
18 1 mopnuni ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}=\bigcup {J}$
19 17 18 syl ${⊢}{\phi }\to {X}=\bigcup {J}$
20 19 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {X}=\bigcup {J}$
21 15 20 sseqtrrd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {k}\subseteq {X}$
22 eleq1 ${⊢}{k}={X}\to \left({k}\in {U}↔{X}\in {U}\right)$
23 22 notbid ${⊢}{k}={X}\to \left(¬{k}\in {U}↔¬{X}\in {U}\right)$
24 7 23 syl5ibrcom ${⊢}{\phi }\to \left({k}={X}\to ¬{k}\in {U}\right)$
25 24 necon2ad ${⊢}{\phi }\to \left({k}\in {U}\to {k}\ne {X}\right)$
26 25 adantr ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to \left({k}\in {U}\to {k}\ne {X}\right)$
27 26 imp ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {k}\ne {X}$
28 pssdifn0 ${⊢}\left({k}\subseteq {X}\wedge {k}\ne {X}\right)\to {X}\setminus {k}\ne \varnothing$
29 21 27 28 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {X}\setminus {k}\ne \varnothing$
30 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)$
31 30 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}⟶ℝ$
32 10 11 29 31 syl3anc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\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}⟶ℝ$
33 30 fmpt ${⊢}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ↔\left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right):{X}⟶ℝ$
34 32 33 sylibr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ$
35 simplr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {y}\in {X}$
36 rsp ${⊢}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ\to \left({y}\in {X}\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ\right)$
37 34 35 36 sylc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ$
38 9 37 fsumrecl ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to \sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ$
39 5 eleq2d ${⊢}{\phi }\to \left({y}\in {X}↔{y}\in \bigcup {U}\right)$
40 39 biimpa ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {y}\in \bigcup {U}$
41 eluni2 ${⊢}{y}\in \bigcup {U}↔\exists {m}\in {U}\phantom{\rule{.4em}{0ex}}{y}\in {m}$
42 40 41 sylib ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to \exists {m}\in {U}\phantom{\rule{.4em}{0ex}}{y}\in {m}$
43 0red ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to 0\in ℝ$
44 simplr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {y}\in {X}$
45 eqid ${⊢}\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)=\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)$
46 45 metdsval ${⊢}{y}\in {X}\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)=sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)$
47 44 46 syl ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)=sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)$
48 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {D}\in \mathrm{Met}\left({X}\right)$
49 difssd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {X}\setminus {m}\subseteq {X}$
50 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {U}\subseteq {J}$
51 simprl ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {m}\in {U}$
52 50 51 sseldd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {m}\in {J}$
53 elssuni ${⊢}{m}\in {J}\to {m}\subseteq \bigcup {J}$
54 52 53 syl ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {m}\subseteq \bigcup {J}$
55 48 16 18 3syl ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {X}=\bigcup {J}$
56 54 55 sseqtrrd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {m}\subseteq {X}$
57 eleq1 ${⊢}{m}={X}\to \left({m}\in {U}↔{X}\in {U}\right)$
58 57 notbid ${⊢}{m}={X}\to \left(¬{m}\in {U}↔¬{X}\in {U}\right)$
59 7 58 syl5ibrcom ${⊢}{\phi }\to \left({m}={X}\to ¬{m}\in {U}\right)$
60 59 necon2ad ${⊢}{\phi }\to \left({m}\in {U}\to {m}\ne {X}\right)$
61 60 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left({m}\in {U}\to {m}\ne {X}\right)$
62 51 61 mpd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {m}\ne {X}$
63 pssdifn0 ${⊢}\left({m}\subseteq {X}\wedge {m}\ne {X}\right)\to {X}\setminus {m}\ne \varnothing$
64 56 62 63 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {X}\setminus {m}\ne \varnothing$
65 45 metdsre ${⊢}\left({D}\in \mathrm{Met}\left({X}\right)\wedge {X}\setminus {m}\subseteq {X}\wedge {X}\setminus {m}\ne \varnothing \right)\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right):{X}⟶ℝ$
66 48 49 64 65 syl3anc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right):{X}⟶ℝ$
67 66 44 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\in ℝ$
68 47 67 eqeltrrd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ$
69 38 adantr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ$
70 17 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
71 45 metdsf ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {X}\setminus {m}\subseteq {X}\right)\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right):{X}⟶\left[0,\mathrm{+\infty }\right]$
72 70 49 71 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right):{X}⟶\left[0,\mathrm{+\infty }\right]$
73 72 44 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\in \left[0,\mathrm{+\infty }\right]$
74 elxrge0 ${⊢}\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\in \left[0,\mathrm{+\infty }\right]↔\left(\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\in {ℝ}^{*}\wedge 0\le \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\right)$
75 73 74 sylib ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left(\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\in {ℝ}^{*}\wedge 0\le \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\right)$
76 75 simprd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to 0\le \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)$
77 elndif ${⊢}{y}\in {m}\to ¬{y}\in \left({X}\setminus {m}\right)$
78 77 ad2antll ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to ¬{y}\in \left({X}\setminus {m}\right)$
79 55 difeq1d ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {X}\setminus {m}=\bigcup {J}\setminus {m}$
80 1 mopntop ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{Top}$
81 70 80 syl ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {J}\in \mathrm{Top}$
82 eqid ${⊢}\bigcup {J}=\bigcup {J}$
83 82 opncld ${⊢}\left({J}\in \mathrm{Top}\wedge {m}\in {J}\right)\to \bigcup {J}\setminus {m}\in \mathrm{Clsd}\left({J}\right)$
84 81 52 83 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \bigcup {J}\setminus {m}\in \mathrm{Clsd}\left({J}\right)$
85 79 84 eqeltrd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {X}\setminus {m}\in \mathrm{Clsd}\left({J}\right)$
86 cldcls ${⊢}{X}\setminus {m}\in \mathrm{Clsd}\left({J}\right)\to \mathrm{cls}\left({J}\right)\left({X}\setminus {m}\right)={X}\setminus {m}$
87 85 86 syl ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \mathrm{cls}\left({J}\right)\left({X}\setminus {m}\right)={X}\setminus {m}$
88 78 87 neleqtrrd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to ¬{y}\in \mathrm{cls}\left({J}\right)\left({X}\setminus {m}\right)$
89 45 1 metdseq0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {X}\setminus {m}\subseteq {X}\wedge {y}\in {X}\right)\to \left(\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)=0↔{y}\in \mathrm{cls}\left({J}\right)\left({X}\setminus {m}\right)\right)$
90 70 49 44 89 syl3anc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left(\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)=0↔{y}\in \mathrm{cls}\left({J}\right)\left({X}\setminus {m}\right)\right)$
91 90 necon3abid ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left(\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\ne 0↔¬{y}\in \mathrm{cls}\left({J}\right)\left({X}\setminus {m}\right)\right)$
92 88 91 mpbird ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to \left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)\ne 0$
93 67 76 92 ne0gt0d ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to 0<\left({w}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{w}{D}{z}\right),{ℝ}^{*},<\right)\right)\left({y}\right)$
94 93 47 breqtrd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to 0
95 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to {U}\in \mathrm{Fin}$
96 37 adantlr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\wedge {k}\in {U}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in ℝ$
97 17 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
98 30 metdsf ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {X}\setminus {k}\subseteq {X}\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}⟶\left[0,\mathrm{+\infty }\right]$
99 97 11 98 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\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}⟶\left[0,\mathrm{+\infty }\right]$
100 30 fmpt ${⊢}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in \left[0,\mathrm{+\infty }\right]↔\left({y}\in {X}⟼sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right):{X}⟶\left[0,\mathrm{+\infty }\right]$
101 99 100 sylibr ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in \left[0,\mathrm{+\infty }\right]$
102 rsp ${⊢}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in \left[0,\mathrm{+\infty }\right]\to \left({y}\in {X}\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in \left[0,\mathrm{+\infty }\right]\right)$
103 101 35 102 sylc ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in \left[0,\mathrm{+\infty }\right]$
104 elxrge0 ${⊢}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in \left[0,\mathrm{+\infty }\right]↔\left(sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge 0\le sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)$
105 103 104 sylib ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to \left(sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge 0\le sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\right)$
106 105 simprd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge {k}\in {U}\right)\to 0\le sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)$
107 106 adantlr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\wedge {k}\in {U}\right)\to 0\le sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)$
108 difeq2 ${⊢}{k}={m}\to {X}\setminus {k}={X}\setminus {m}$
109 108 mpteq1d ${⊢}{k}={m}\to \left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right)=\left({z}\in \left({X}\setminus {m}\right)⟼{y}{D}{z}\right)$
110 109 rneqd ${⊢}{k}={m}\to \mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right)=\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{y}{D}{z}\right)$
111 110 infeq1d ${⊢}{k}={m}\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 {m}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)$
112 95 96 107 111 51 fsumge1 ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {m}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\le \sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)$
113 43 68 69 94 112 ltletrd ${⊢}\left(\left({\phi }\wedge {y}\in {X}\right)\wedge \left({m}\in {U}\wedge {y}\in {m}\right)\right)\to 0<\sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)$
114 42 113 rexlimddv ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to 0<\sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)$
115 38 114 elrpd ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to \sum _{{k}\in {U}}sup\left(\mathrm{ran}\left({z}\in \left({X}\setminus {k}\right)⟼{y}{D}{z}\right),{ℝ}^{*},<\right)\in {ℝ}^{+}$
116 115 8 fmptd ${⊢}{\phi }\to {F}:{X}⟶{ℝ}^{+}$