# Metamath Proof Explorer

## Theorem blrnps

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) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blrnps ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to \left({A}\in \mathrm{ran}\mathrm{ball}\left({D}\right)↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{A}={x}\mathrm{ball}\left({D}\right){r}\right)$

### Proof

Step Hyp Ref Expression
1 blfps ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to \mathrm{ball}\left({D}\right):{X}×{ℝ}^{*}⟶𝒫{X}$
2 ffn ${⊢}\mathrm{ball}\left({D}\right):{X}×{ℝ}^{*}⟶𝒫{X}\to \mathrm{ball}\left({D}\right)Fn\left({X}×{ℝ}^{*}\right)$
3 ovelrn ${⊢}\mathrm{ball}\left({D}\right)Fn\left({X}×{ℝ}^{*}\right)\to \left({A}\in \mathrm{ran}\mathrm{ball}\left({D}\right)↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{A}={x}\mathrm{ball}\left({D}\right){r}\right)$
4 1 2 3 3syl ${⊢}{D}\in \mathrm{PsMet}\left({X}\right)\to \left({A}\in \mathrm{ran}\mathrm{ball}\left({D}\right)↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{A}={x}\mathrm{ball}\left({D}\right){r}\right)$