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

Metamath Proof Explorer

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 ‘ 𝐷 ) 𝑆 ) ⊆ [ 𝑃 ] ∼ )