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

Metamath Proof Explorer

Theorem blssm

Description: A ball is a subset of the base set of a metric space. (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Assertion	blssm	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \subseteq X$

Step	Hyp	Ref	Expression
1		blf	$⊢ D \in ∞Met (X) \to ball (D) : X \times ℝ^{*} ⟶ 𝒫 X$
2		fovcdm	$⊢ (ball (D) : X \times ℝ^{} ⟶ 𝒫 X \land P \in X \land R \in ℝ^{}) \to P ball (D) R \in 𝒫 X$
3	1 2	syl3an1	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \in 𝒫 X$
4	3	elpwid	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \subseteq X$