Theorem blssec

Description: A ball centered at P is contained in the set of points finitely separated from P . This is just an application of ssbl to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypothesis	xmeter.1	⊢ ∼ = ( ◡ 𝐷 “ ℝ )
Assertion	blssec	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ⊆ [ 𝑃 ] ∼ )

Proof

Step	Hyp	Ref	Expression
1		xmeter.1	⊢ ∼ = ( ◡ 𝐷 “ ℝ )
2		pnfge	⊢ ( 𝑆 ∈ ℝ* → 𝑆 ≤ +∞ )
3	2	adantl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑆 ∈ ℝ* ) → 𝑆 ≤ +∞ )
4		pnfxr	⊢ +∞ ∈ ℝ*
5		ssbl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑆 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ 𝑆 ≤ +∞ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
6	5	3expia	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑆 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ) → ( 𝑆 ≤ +∞ → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) )
7	4 6	mpanr2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑆 ∈ ℝ* ) → ( 𝑆 ≤ +∞ → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) )
8	3 7	mpd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑆 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
9	8	3impa	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
10	1	xmetec	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → [ 𝑃 ] ∼ = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
11	10	3adant3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ) → [ 𝑃 ] ∼ = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )
12	9 11	sseqtrrd	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ⊆ [ 𝑃 ] ∼ )