# Metamath Proof Explorer

## Theorem blf

Description: Mapping of a ball. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion blf ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{ball}\left({D}\right):{X}×{ℝ}^{*}⟶𝒫{X}$

### Proof

Step Hyp Ref Expression
1 ssrab2 ${⊢}\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\subseteq {X}$
2 elfvdm ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}\in \mathrm{dom}\mathrm{\infty Met}$
3 elpw2g ${⊢}{X}\in \mathrm{dom}\mathrm{\infty Met}\to \left(\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\in 𝒫{X}↔\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\subseteq {X}\right)$
4 2 3 syl ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\in 𝒫{X}↔\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\subseteq {X}\right)$
5 1 4 mpbiri ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\in 𝒫{X}$
6 5 a1d ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(\left({x}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to \left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\in 𝒫{X}\right)$
7 6 ralrimivv ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {r}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\in 𝒫{X}$
8 eqid ${⊢}\left({x}\in {X},{r}\in {ℝ}^{*}⟼\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\right)=\left({x}\in {X},{r}\in {ℝ}^{*}⟼\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\right)$
9 8 fmpo ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {r}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\in 𝒫{X}↔\left({x}\in {X},{r}\in {ℝ}^{*}⟼\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\right):{X}×{ℝ}^{*}⟶𝒫{X}$
10 7 9 sylib ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({x}\in {X},{r}\in {ℝ}^{*}⟼\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\right):{X}×{ℝ}^{*}⟶𝒫{X}$
11 blfval ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{ball}\left({D}\right)=\left({x}\in {X},{r}\in {ℝ}^{*}⟼\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\right)$
12 11 feq1d ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(\mathrm{ball}\left({D}\right):{X}×{ℝ}^{*}⟶𝒫{X}↔\left({x}\in {X},{r}\in {ℝ}^{*}⟼\left\{{y}\in {X}|{x}{D}{y}<{r}\right\}\right):{X}×{ℝ}^{*}⟶𝒫{X}\right)$
13 10 12 mpbird ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{ball}\left({D}\right):{X}×{ℝ}^{*}⟶𝒫{X}$