# Metamath Proof Explorer

## Theorem metdseq0

Description: The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses metdscn.f ${⊢}{F}=\left({x}\in {X}⟼sup\left(\mathrm{ran}\left({y}\in {S}⟼{x}{D}{y}\right),{ℝ}^{*},<\right)\right)$
metdscn.j ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
Assertion metdseq0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to \left({F}\left({A}\right)=0↔{A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 metdscn.f ${⊢}{F}=\left({x}\in {X}⟼sup\left(\mathrm{ran}\left({y}\in {S}⟼{x}{D}{y}\right),{ℝ}^{*},<\right)\right)$
2 metdscn.j ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
3 simpll1 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
4 simprl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\to {z}\in {J}$
5 simprr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\to {A}\in {z}$
6 2 mopni2 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {z}\in {J}\wedge {A}\in {z}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}\mathrm{ball}\left({D}\right){r}\subseteq {z}$
7 3 4 5 6 syl3anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}\mathrm{ball}\left({D}\right){r}\subseteq {z}$
8 simprr ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}$
9 8 ssrind ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to \left({A}\mathrm{ball}\left({D}\right){r}\right)\cap {S}\subseteq {z}\cap {S}$
10 rpgt0 ${⊢}{r}\in {ℝ}^{+}\to 0<{r}$
11 0re ${⊢}0\in ℝ$
12 rpre ${⊢}{r}\in {ℝ}^{+}\to {r}\in ℝ$
13 ltnle ${⊢}\left(0\in ℝ\wedge {r}\in ℝ\right)\to \left(0<{r}↔¬{r}\le 0\right)$
14 11 12 13 sylancr ${⊢}{r}\in {ℝ}^{+}\to \left(0<{r}↔¬{r}\le 0\right)$
15 10 14 mpbid ${⊢}{r}\in {ℝ}^{+}\to ¬{r}\le 0$
16 15 ad2antrl ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to ¬{r}\le 0$
17 simpllr ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to {F}\left({A}\right)=0$
18 17 breq2d ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to \left({r}\le {F}\left({A}\right)↔{r}\le 0\right)$
19 3 adantr ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
20 simpl2 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to {S}\subseteq {X}$
21 20 ad2antrr ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to {S}\subseteq {X}$
22 simpl3 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to {A}\in {X}$
23 22 ad2antrr ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to {A}\in {X}$
24 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
25 24 ad2antrl ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to {r}\in {ℝ}^{*}$
26 1 metdsge ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {r}\in {ℝ}^{*}\right)\to \left({r}\le {F}\left({A}\right)↔{S}\cap \left({A}\mathrm{ball}\left({D}\right){r}\right)=\varnothing \right)$
27 19 21 23 25 26 syl31anc ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to \left({r}\le {F}\left({A}\right)↔{S}\cap \left({A}\mathrm{ball}\left({D}\right){r}\right)=\varnothing \right)$
28 18 27 bitr3d ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to \left({r}\le 0↔{S}\cap \left({A}\mathrm{ball}\left({D}\right){r}\right)=\varnothing \right)$
29 incom ${⊢}{S}\cap \left({A}\mathrm{ball}\left({D}\right){r}\right)=\left({A}\mathrm{ball}\left({D}\right){r}\right)\cap {S}$
30 29 eqeq1i ${⊢}{S}\cap \left({A}\mathrm{ball}\left({D}\right){r}\right)=\varnothing ↔\left({A}\mathrm{ball}\left({D}\right){r}\right)\cap {S}=\varnothing$
31 28 30 syl6bb ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to \left({r}\le 0↔\left({A}\mathrm{ball}\left({D}\right){r}\right)\cap {S}=\varnothing \right)$
32 31 necon3bbid ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to \left(¬{r}\le 0↔\left({A}\mathrm{ball}\left({D}\right){r}\right)\cap {S}\ne \varnothing \right)$
33 16 32 mpbid ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to \left({A}\mathrm{ball}\left({D}\right){r}\right)\cap {S}\ne \varnothing$
34 ssn0 ${⊢}\left(\left({A}\mathrm{ball}\left({D}\right){r}\right)\cap {S}\subseteq {z}\cap {S}\wedge \left({A}\mathrm{ball}\left({D}\right){r}\right)\cap {S}\ne \varnothing \right)\to {z}\cap {S}\ne \varnothing$
35 9 33 34 syl2anc ${⊢}\left(\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\wedge \left({r}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left({D}\right){r}\subseteq {z}\right)\right)\to {z}\cap {S}\ne \varnothing$
36 7 35 rexlimddv ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge \left({z}\in {J}\wedge {A}\in {z}\right)\right)\to {z}\cap {S}\ne \varnothing$
37 36 expr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\wedge {z}\in {J}\right)\to \left({A}\in {z}\to {z}\cap {S}\ne \varnothing \right)$
38 37 ralrimiva ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to \forall {z}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {z}\to {z}\cap {S}\ne \varnothing \right)$
39 2 mopntopon ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
40 39 3ad2ant1 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
41 40 adantr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
42 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
43 41 42 syl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to {J}\in \mathrm{Top}$
44 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
45 41 44 syl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to {X}=\bigcup {J}$
46 20 45 sseqtrd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to {S}\subseteq \bigcup {J}$
47 22 45 eleqtrd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to {A}\in \bigcup {J}$
48 eqid ${⊢}\bigcup {J}=\bigcup {J}$
49 48 elcls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq \bigcup {J}\wedge {A}\in \bigcup {J}\right)\to \left({A}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\forall {z}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {z}\to {z}\cap {S}\ne \varnothing \right)\right)$
50 43 46 47 49 syl3anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to \left({A}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\forall {z}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {z}\to {z}\cap {S}\ne \varnothing \right)\right)$
51 38 50 mpbird ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)=0\right)\to {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)$
52 incom ${⊢}\left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)\cap {S}={S}\cap \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)$
53 1 metdsf ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\to {F}:{X}⟶\left[0,\mathrm{+\infty }\right]$
54 53 ffvelrnda ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge {A}\in {X}\right)\to {F}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]$
55 54 3impa ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to {F}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]$
56 eliccxr ${⊢}{F}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]\to {F}\left({A}\right)\in {ℝ}^{*}$
57 55 56 syl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to {F}\left({A}\right)\in {ℝ}^{*}$
58 57 xrleidd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to {F}\left({A}\right)\le {F}\left({A}\right)$
59 1 metdsge ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {F}\left({A}\right)\in {ℝ}^{*}\right)\to \left({F}\left({A}\right)\le {F}\left({A}\right)↔{S}\cap \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)=\varnothing \right)$
60 57 59 mpdan ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to \left({F}\left({A}\right)\le {F}\left({A}\right)↔{S}\cap \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)=\varnothing \right)$
61 58 60 mpbid ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to {S}\cap \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)=\varnothing$
62 52 61 syl5eq ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)\cap {S}=\varnothing$
63 62 adantr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)\cap {S}=\varnothing$
64 40 ad2antrr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
65 64 42 syl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {J}\in \mathrm{Top}$
66 simpll2 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {S}\subseteq {X}$
67 64 44 syl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {X}=\bigcup {J}$
68 66 67 sseqtrd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {S}\subseteq \bigcup {J}$
69 simplr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)$
70 simpll1 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
71 simpll3 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {A}\in {X}$
72 57 ad2antrr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {F}\left({A}\right)\in {ℝ}^{*}$
73 2 blopn ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {F}\left({A}\right)\in {ℝ}^{*}\right)\to {A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\in {J}$
74 70 71 72 73 syl3anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\in {J}$
75 simpr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to 0<{F}\left({A}\right)$
76 xblcntr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge \left({F}\left({A}\right)\in {ℝ}^{*}\wedge 0<{F}\left({A}\right)\right)\right)\to {A}\in \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)$
77 70 71 72 75 76 syl112anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to {A}\in \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)$
78 48 clsndisj ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq \bigcup {J}\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\in {J}\wedge {A}\in \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)\right)\right)\to \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)\cap {S}\ne \varnothing$
79 65 68 69 74 77 78 syl32anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge 0<{F}\left({A}\right)\right)\to \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)\cap {S}\ne \varnothing$
80 79 ex ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left(0<{F}\left({A}\right)\to \left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)\cap {S}\ne \varnothing \right)$
81 80 necon2bd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left(\left({A}\mathrm{ball}\left({D}\right){F}\left({A}\right)\right)\cap {S}=\varnothing \to ¬0<{F}\left({A}\right)\right)$
82 63 81 mpd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to ¬0<{F}\left({A}\right)$
83 elxrge0 ${⊢}{F}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]↔\left({F}\left({A}\right)\in {ℝ}^{*}\wedge 0\le {F}\left({A}\right)\right)$
84 83 simprbi ${⊢}{F}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]\to 0\le {F}\left({A}\right)$
85 55 84 syl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to 0\le {F}\left({A}\right)$
86 0xr ${⊢}0\in {ℝ}^{*}$
87 xrleloe ${⊢}\left(0\in {ℝ}^{*}\wedge {F}\left({A}\right)\in {ℝ}^{*}\right)\to \left(0\le {F}\left({A}\right)↔\left(0<{F}\left({A}\right)\vee 0={F}\left({A}\right)\right)\right)$
88 86 57 87 sylancr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to \left(0\le {F}\left({A}\right)↔\left(0<{F}\left({A}\right)\vee 0={F}\left({A}\right)\right)\right)$
89 85 88 mpbid ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to \left(0<{F}\left({A}\right)\vee 0={F}\left({A}\right)\right)$
90 89 adantr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left(0<{F}\left({A}\right)\vee 0={F}\left({A}\right)\right)$
91 90 ord ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left(¬0<{F}\left({A}\right)\to 0={F}\left({A}\right)\right)$
92 82 91 mpd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to 0={F}\left({A}\right)$
93 92 eqcomd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\wedge {A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {F}\left({A}\right)=0$
94 51 93 impbida ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {X}\right)\to \left({F}\left({A}\right)=0↔{A}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)$