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 β€˜ 𝐽 ) )