Theorem blrn

Description: Membership in the range of the ball function. Note that ran ( ballD ) is the collection of all balls for metric D . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013)

	Ref	Expression
Assertion	blrn	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(A\in \mathrm{ran}\mathrm{ball}\left(D\right)\leftrightarrow \exists x\in X\exists r\in {ℝ}^{*}A=x\mathrm{ball}\left(D\right)r\right)$$

Proof

Step	Hyp	Ref	Expression
1		blf	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{ball}\left(D\right):X\times {ℝ}^{*}⟶𝒫X$$
2		ffn	$$⊢\mathrm{ball}\left(D\right):X\times {ℝ}^{*}⟶𝒫X\to \mathrm{ball}\left(D\right)Fn\left(X\times {ℝ}^{*}\right)$$
3		ovelrn	$$⊢\mathrm{ball}\left(D\right)Fn\left(X\times {ℝ}^{*}\right)\to \left(A\in \mathrm{ran}\mathrm{ball}\left(D\right)\leftrightarrow \exists x\in X\exists r\in {ℝ}^{*}A=x\mathrm{ball}\left(D\right)r\right)$$
4	1 2 3	3syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(A\in \mathrm{ran}\mathrm{ball}\left(D\right)\leftrightarrow \exists x\in X\exists r\in {ℝ}^{*}A=x\mathrm{ball}\left(D\right)r\right)$$