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	$⊢ \underset{˙}{\sim} = D^{-1} [ℝ]$
	Assertion	blssec	$⊢ (D \in ∞Met (X) \land P \in X \land S \in ℝ^{*}) \to P ball (D) S \subseteq [P] \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		xmeter.1	$⊢ \underset{˙}{\sim} = D^{-1} [ℝ]$
2		pnfge	$⊢ S \in ℝ^{*} \to S \leq +∞$
3	2	adantl	$⊢ ((D \in ∞Met (X) \land P \in X) \land S \in ℝ^{*}) \to S \leq +∞$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5		ssbl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (S \in ℝ^{} \land +∞ \in ℝ^{}) \land S \leq +∞) \to P ball (D) S \subseteq P ball (D) +∞$
6	5	3expia	$⊢ ((D \in ∞Met (X) \land P \in X) \land (S \in ℝ^{} \land +∞ \in ℝ^{})) \to (S \leq +∞ \to P ball (D) S \subseteq P ball (D) +∞)$
7	4 6	mpanr2	$⊢ ((D \in ∞Met (X) \land P \in X) \land S \in ℝ^{*}) \to (S \leq +∞ \to P ball (D) S \subseteq P ball (D) +∞)$
8	3 7	mpd	$⊢ ((D \in ∞Met (X) \land P \in X) \land S \in ℝ^{*}) \to P ball (D) S \subseteq P ball (D) +∞$
9	8	3impa	$⊢ (D \in ∞Met (X) \land P \in X \land S \in ℝ^{*}) \to P ball (D) S \subseteq P ball (D) +∞$
10	1	xmetec	$⊢ (D \in ∞Met (X) \land P \in X) \to [P] \underset{˙}{\sim} = P ball (D) +∞$
11	10	3adant3	$⊢ (D \in ∞Met (X) \land P \in X \land S \in ℝ^{*}) \to [P] \underset{˙}{\sim} = P ball (D) +∞$
12	9 11	sseqtrrd	$⊢ (D \in ∞Met (X) \land P \in X \land S \in ℝ^{*}) \to P ball (D) S \subseteq [P] \underset{˙}{\sim}$