Metamath Proof Explorer

Theorem blcld

Description: A "closed ball" in a metric space is actually closed. (Contributed by Mario Carneiro, 31-Dec-2013) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypotheses mopni.1 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
blcld.3 ${⊢}{S}=\left\{{z}\in {X}|{P}{D}{z}\le {R}\right\}$
Assertion blcld ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {S}\in \mathrm{Clsd}\left({J}\right)$

Proof

Step Hyp Ref Expression
1 mopni.1 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 blcld.3 ${⊢}{S}=\left\{{z}\in {X}|{P}{D}{z}\le {R}\right\}$
3 1 mopnuni ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}=\bigcup {J}$
4 3 3ad2ant1 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {X}=\bigcup {J}$
5 4 difeq1d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {X}\setminus {S}=\bigcup {J}\setminus {S}$
6 difssd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {X}\setminus {S}\subseteq {X}$
7 simpl3 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to {R}\in {ℝ}^{*}$
8 simpl1 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
9 simpl2 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to {P}\in {X}$
10 eldifi ${⊢}{y}\in \left({X}\setminus {S}\right)\to {y}\in {X}$
11 10 adantl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to {y}\in {X}$
12 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {y}\in {X}\right)\to {P}{D}{y}\in {ℝ}^{*}$
13 8 9 11 12 syl3anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to {P}{D}{y}\in {ℝ}^{*}$
14 eldif ${⊢}{y}\in \left({X}\setminus {S}\right)↔\left({y}\in {X}\wedge ¬{y}\in {S}\right)$
15 oveq2 ${⊢}{z}={y}\to {P}{D}{z}={P}{D}{y}$
16 15 breq1d ${⊢}{z}={y}\to \left({P}{D}{z}\le {R}↔{P}{D}{y}\le {R}\right)$
17 16 2 elrab2 ${⊢}{y}\in {S}↔\left({y}\in {X}\wedge {P}{D}{y}\le {R}\right)$
18 17 simplbi2 ${⊢}{y}\in {X}\to \left({P}{D}{y}\le {R}\to {y}\in {S}\right)$
19 18 con3dimp ${⊢}\left({y}\in {X}\wedge ¬{y}\in {S}\right)\to ¬{P}{D}{y}\le {R}$
20 14 19 sylbi ${⊢}{y}\in \left({X}\setminus {S}\right)\to ¬{P}{D}{y}\le {R}$
21 20 adantl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to ¬{P}{D}{y}\le {R}$
22 xrltnle ${⊢}\left({R}\in {ℝ}^{*}\wedge {P}{D}{y}\in {ℝ}^{*}\right)\to \left({R}<{P}{D}{y}↔¬{P}{D}{y}\le {R}\right)$
23 7 13 22 syl2anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to \left({R}<{P}{D}{y}↔¬{P}{D}{y}\le {R}\right)$
24 21 23 mpbird ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to {R}<{P}{D}{y}$
25 qbtwnxr ${⊢}\left({R}\in {ℝ}^{*}\wedge {P}{D}{y}\in {ℝ}^{*}\wedge {R}<{P}{D}{y}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({R}<{x}\wedge {x}<{P}{D}{y}\right)$
26 7 13 24 25 syl3anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({R}<{x}\wedge {x}<{P}{D}{y}\right)$
27 qre ${⊢}{x}\in ℚ\to {x}\in ℝ$
28 8 adantr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
29 11 adantr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {y}\in {X}$
30 13 adantr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {P}{D}{y}\in {ℝ}^{*}$
31 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
32 31 ad2antrl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {x}\in {ℝ}^{*}$
33 32 xnegcld ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to -{x}\in {ℝ}^{*}$
34 30 33 xaddcld ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to \left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\in {ℝ}^{*}$
35 blelrn ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge \left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\in \mathrm{ran}\mathrm{ball}\left({D}\right)$
36 28 29 34 35 syl3anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\in \mathrm{ran}\mathrm{ball}\left({D}\right)$
37 simprrr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {x}<{P}{D}{y}$
38 xposdif ${⊢}\left({x}\in {ℝ}^{*}\wedge {P}{D}{y}\in {ℝ}^{*}\right)\to \left({x}<{P}{D}{y}↔0<\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)$
39 32 30 38 syl2anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to \left({x}<{P}{D}{y}↔0<\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)$
40 37 39 mpbid ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to 0<\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)$
41 xblcntr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge \left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\in {ℝ}^{*}\wedge 0<\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)\to {y}\in \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)$
42 28 29 34 40 41 syl112anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {y}\in \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)$
43 incom ${⊢}\left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)\cap \left({P}\mathrm{ball}\left({D}\right){x}\right)=\left({P}\mathrm{ball}\left({D}\right){x}\right)\cap \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)$
44 9 adantr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {P}\in {X}$
45 xaddcom ${⊢}\left({x}\in {ℝ}^{*}\wedge \left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\in {ℝ}^{*}\right)\to {x}{+}_{𝑒}\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)=\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right){+}_{𝑒}{x}$
46 32 34 45 syl2anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {x}{+}_{𝑒}\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)=\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right){+}_{𝑒}{x}$
47 simprl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {x}\in ℝ$
48 xnpcan ${⊢}\left({P}{D}{y}\in {ℝ}^{*}\wedge {x}\in ℝ\right)\to \left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right){+}_{𝑒}{x}={P}{D}{y}$
49 30 47 48 syl2anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to \left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right){+}_{𝑒}{x}={P}{D}{y}$
50 46 49 eqtrd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {x}{+}_{𝑒}\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)={P}{D}{y}$
51 30 xrleidd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {P}{D}{y}\le {P}{D}{y}$
52 50 51 eqbrtrd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {x}{+}_{𝑒}\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\le {P}{D}{y}$
53 bldisj ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {y}\in {X}\right)\wedge \left({x}\in {ℝ}^{*}\wedge \left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\in {ℝ}^{*}\wedge {x}{+}_{𝑒}\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\le {P}{D}{y}\right)\right)\to \left({P}\mathrm{ball}\left({D}\right){x}\right)\cap \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)=\varnothing$
54 28 44 29 32 34 52 53 syl33anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to \left({P}\mathrm{ball}\left({D}\right){x}\right)\cap \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)=\varnothing$
55 43 54 syl5eq ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)\cap \left({P}\mathrm{ball}\left({D}\right){x}\right)=\varnothing$
56 blssm ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge \left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}$
57 28 29 34 56 syl3anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}$
58 reldisj ${⊢}{y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}\to \left(\left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)\cap \left({P}\mathrm{ball}\left({D}\right){x}\right)=\varnothing ↔{y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}\setminus \left({P}\mathrm{ball}\left({D}\right){x}\right)\right)$
59 57 58 syl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to \left(\left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)\cap \left({P}\mathrm{ball}\left({D}\right){x}\right)=\varnothing ↔{y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}\setminus \left({P}\mathrm{ball}\left({D}\right){x}\right)\right)$
60 55 59 mpbid ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}\setminus \left({P}\mathrm{ball}\left({D}\right){x}\right)$
61 7 adantr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {R}\in {ℝ}^{*}$
62 simprrl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {R}<{x}$
63 1 2 blsscls2 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge \left({R}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\wedge {R}<{x}\right)\right)\to {S}\subseteq {P}\mathrm{ball}\left({D}\right){x}$
64 28 44 61 32 62 63 syl23anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {S}\subseteq {P}\mathrm{ball}\left({D}\right){x}$
65 64 sscond ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {X}\setminus \left({P}\mathrm{ball}\left({D}\right){x}\right)\subseteq {X}\setminus {S}$
66 60 65 sstrd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to {y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}\setminus {S}$
67 eleq2 ${⊢}{w}={y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\to \left({y}\in {w}↔{y}\in \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)\right)$
68 sseq1 ${⊢}{w}={y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\to \left({w}\subseteq {X}\setminus {S}↔{y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}\setminus {S}\right)$
69 67 68 anbi12d ${⊢}{w}={y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\to \left(\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)↔\left({y}\in \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)\wedge {y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}\setminus {S}\right)\right)$
70 69 rspcev ${⊢}\left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\in \mathrm{ran}\mathrm{ball}\left({D}\right)\wedge \left({y}\in \left({y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\right)\wedge {y}\mathrm{ball}\left({D}\right)\left(\left({P}{D}{y}\right){+}_{𝑒}\left(-{x}\right)\right)\subseteq {X}\setminus {S}\right)\right)\to \exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)$
71 36 42 66 70 syl12anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge \left({x}\in ℝ\wedge \left({R}<{x}\wedge {x}<{P}{D}{y}\right)\right)\right)\to \exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)$
72 71 expr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge {x}\in ℝ\right)\to \left(\left({R}<{x}\wedge {x}<{P}{D}{y}\right)\to \exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)\right)$
73 27 72 sylan2 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\wedge {x}\in ℚ\right)\to \left(\left({R}<{x}\wedge {x}<{P}{D}{y}\right)\to \exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)\right)$
74 73 rexlimdva ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to \left(\exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({R}<{x}\wedge {x}<{P}{D}{y}\right)\to \exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)\right)$
75 26 74 mpd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {y}\in \left({X}\setminus {S}\right)\right)\to \exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)$
76 75 ralrimiva ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to \forall {y}\in \left({X}\setminus {S}\right)\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)$
77 1 elmopn ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({X}\setminus {S}\in {J}↔\left({X}\setminus {S}\subseteq {X}\wedge \forall {y}\in \left({X}\setminus {S}\right)\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)\right)\right)$
78 77 3ad2ant1 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to \left({X}\setminus {S}\in {J}↔\left({X}\setminus {S}\subseteq {X}\wedge \forall {y}\in \left({X}\setminus {S}\right)\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {w}\wedge {w}\subseteq {X}\setminus {S}\right)\right)\right)$
79 6 76 78 mpbir2and ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {X}\setminus {S}\in {J}$
80 5 79 eqeltrrd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to \bigcup {J}\setminus {S}\in {J}$
81 1 mopntop ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{Top}$
82 81 3ad2ant1 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {J}\in \mathrm{Top}$
83 2 ssrab3 ${⊢}{S}\subseteq {X}$
84 83 4 sseqtrid ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {S}\subseteq \bigcup {J}$
85 eqid ${⊢}\bigcup {J}=\bigcup {J}$
86 85 iscld2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq \bigcup {J}\right)\to \left({S}\in \mathrm{Clsd}\left({J}\right)↔\bigcup {J}\setminus {S}\in {J}\right)$
87 82 84 86 syl2anc ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to \left({S}\in \mathrm{Clsd}\left({J}\right)↔\bigcup {J}\setminus {S}\in {J}\right)$
88 80 87 mpbird ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {S}\in \mathrm{Clsd}\left({J}\right)$