Metamath Proof Explorer

Theorem blelrn

Description: A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

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

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