This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
blcld.3 ⊢ 𝑆 = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 }
Assertion blcld ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 blcld.3 ⊢ 𝑆 = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 }
3 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
4 3 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝑋 = ∪ 𝐽 )
5 4 difeq1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑋 ∖ 𝑆 ) = ( ∪ 𝐽 ∖ 𝑆 ) )
6 difssd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋 )
7 simpl3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → 𝑅 ∈ ℝ* )
8 simpl1 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
9 simpl2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → 𝑃 ∈ 𝑋 )
10 eldifi ⊢ ( 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) → 𝑦 ∈ 𝑋 )
11 10 adantl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → 𝑦 ∈ 𝑋 )
12 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ* )
13 8 9 11 12 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ* )
14 eldif ⊢ ( 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ↔ ( 𝑦 ∈ 𝑋 ∧ ¬ 𝑦 ∈ 𝑆 ) )
15 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑃 𝐷 𝑧 ) = ( 𝑃 𝐷 𝑦 ) )
16 15 breq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ↔ ( 𝑃 𝐷 𝑦 ) ≤ 𝑅 ) )
17 16 2 elrab2 ⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑦 ) ≤ 𝑅 ) )
18 17 simplbi2 ⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝑃 𝐷 𝑦 ) ≤ 𝑅 → 𝑦 ∈ 𝑆 ) )
19 18 con3dimp ⊢ ( ( 𝑦 ∈ 𝑋 ∧ ¬ 𝑦 ∈ 𝑆 ) → ¬ ( 𝑃 𝐷 𝑦 ) ≤ 𝑅 )
20 14 19 sylbi ⊢ ( 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) → ¬ ( 𝑃 𝐷 𝑦 ) ≤ 𝑅 )
21 20 adantl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → ¬ ( 𝑃 𝐷 𝑦 ) ≤ 𝑅 )
22 xrltnle ⊢ ( ( 𝑅 ∈ ℝ* ∧ ( 𝑃 𝐷 𝑦 ) ∈ ℝ* ) → ( 𝑅 < ( 𝑃 𝐷 𝑦 ) ↔ ¬ ( 𝑃 𝐷 𝑦 ) ≤ 𝑅 ) )
23 7 13 22 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → ( 𝑅 < ( 𝑃 𝐷 𝑦 ) ↔ ¬ ( 𝑃 𝐷 𝑦 ) ≤ 𝑅 ) )
24 21 23 mpbird ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → 𝑅 < ( 𝑃 𝐷 𝑦 ) )
25 qbtwnxr ⊢ ( ( 𝑅 ∈ ℝ* ∧ ( 𝑃 𝐷 𝑦 ) ∈ ℝ* ∧ 𝑅 < ( 𝑃 𝐷 𝑦 ) ) → ∃ 𝑥 ∈ ℚ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) )
26 7 13 24 25 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → ∃ 𝑥 ∈ ℚ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) )
27 qre ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
28 8 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
29 11 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑦 ∈ 𝑋 )
30 13 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ* )
31 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
32 31 ad2antrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑥 ∈ ℝ* )
33 32 xnegcld ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → -𝑒 𝑥 ∈ ℝ* )
34 30 33 xaddcld ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ∈ ℝ* )
35 blelrn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∈ ran ( ball ‘ 𝐷 ) )
36 28 29 34 35 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∈ ran ( ball ‘ 𝐷 ) )
37 simprrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑥 < ( 𝑃 𝐷 𝑦 ) )
38 xposdif ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑃 𝐷 𝑦 ) ∈ ℝ* ) → ( 𝑥 < ( 𝑃 𝐷 𝑦 ) ↔ 0 < ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) )
39 32 30 38 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑥 < ( 𝑃 𝐷 𝑦 ) ↔ 0 < ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) )
40 37 39 mpbid ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 0 < ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) )
41 xblcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ∈ ℝ* ∧ 0 < ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ) → 𝑦 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) )
42 28 29 34 40 41 syl112anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑦 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) )
43 incom ⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) = ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) )
44 9 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑃 ∈ 𝑋 )
45 xaddcom ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ∈ ℝ* ) → ( 𝑥 +𝑒 ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) = ( ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) +𝑒 𝑥 ) )
46 32 34 45 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑥 +𝑒 ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) = ( ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) +𝑒 𝑥 ) )
47 simprl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑥 ∈ ℝ )
48 xnpcan ⊢ ( ( ( 𝑃 𝐷 𝑦 ) ∈ ℝ* ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) +𝑒 𝑥 ) = ( 𝑃 𝐷 𝑦 ) )
49 30 47 48 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) +𝑒 𝑥 ) = ( 𝑃 𝐷 𝑦 ) )
50 46 49 eqtrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑥 +𝑒 ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) = ( 𝑃 𝐷 𝑦 ) )
51 30 xrleidd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑃 𝐷 𝑦 ) ≤ ( 𝑃 𝐷 𝑦 ) )
52 50 51 eqbrtrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑥 +𝑒 ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ≤ ( 𝑃 𝐷 𝑦 ) )
53 bldisj ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 ∈ ℝ* ∧ ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ∈ ℝ* ∧ ( 𝑥 +𝑒 ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ≤ ( 𝑃 𝐷 𝑦 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ) = ∅ )
54 28 44 29 32 34 52 53 syl33anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ) = ∅ )
55 43 54 eqtrid ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) = ∅ )
56 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ 𝑋 )
57 28 29 34 56 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ 𝑋 )
58 reldisj ⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ 𝑋 → ( ( ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) = ∅ ↔ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ ( 𝑋 ∖ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
59 57 58 syl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( ( ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) = ∅ ↔ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ ( 𝑋 ∖ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
60 55 59 mpbid ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ ( 𝑋 ∖ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
61 7 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑅 ∈ ℝ* )
62 simprrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑅 < 𝑥 )
63 1 2 blsscls2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑅 < 𝑥 ) ) → 𝑆 ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) )
64 28 44 61 32 62 63 syl23anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → 𝑆 ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) )
65 64 sscond ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑋 ∖ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ⊆ ( 𝑋 ∖ 𝑆 ) )
66 60 65 sstrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ ( 𝑋 ∖ 𝑆 ) )
67 eleq2 ⊢ ( 𝑤 = ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ) )
68 sseq1 ⊢ ( 𝑤 = ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) → ( 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ↔ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
69 67 68 anbi12d ⊢ ( 𝑤 = ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) → ( ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) ↔ ( 𝑦 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ) )
70 69 rspcev ⊢ ( ( ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝑦 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑃 𝐷 𝑦 ) +𝑒 -𝑒 𝑥 ) ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) )
71 36 42 66 70 syl12anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) ) ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) )
72 71 expr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) )
73 27 72 sylan2 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) ∧ 𝑥 ∈ ℚ ) → ( ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) )
74 73 rexlimdva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → ( ∃ 𝑥 ∈ ℚ ( 𝑅 < 𝑥 ∧ 𝑥 < ( 𝑃 𝐷 𝑦 ) ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) )
75 26 74 mpd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ) → ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) )
76 75 ralrimiva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) )
77 1 elmopn ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ↔ ( ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) ) )
78 77 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ↔ ( ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑆 ) ∃ 𝑤 ∈ ran ( ball ‘ 𝐷 ) ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) ) )
79 6 76 78 mpbir2and ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 )
80 5 79 eqeltrrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ∪ 𝐽 ∖ 𝑆 ) ∈ 𝐽 )
81 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
82 81 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝐽 ∈ Top )
83 2 ssrab3 ⊢ 𝑆 ⊆ 𝑋
84 83 4 sseqtrid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝑆 ⊆ ∪ 𝐽 )
85 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
86 85 iscld2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ 𝑆 ) ∈ 𝐽 ) )
87 82 84 86 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ 𝑆 ) ∈ 𝐽 ) )
88 80 87 mpbird ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )