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	syl5eq	⊢ ( ( ( ( 𝐷 ∈ ( ∞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 ‘ 𝐽 ) )