# Metamath Proof Explorer

## Theorem isbnd

Description: The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion isbnd ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$

### Proof

Step Hyp Ref Expression
1 elfvex ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to {X}\in \mathrm{V}$
2 elfvex ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {X}\in \mathrm{V}$
3 2 adantr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)\to {X}\in \mathrm{V}$
4 fveq2 ${⊢}{y}={X}\to \mathrm{Met}\left({y}\right)=\mathrm{Met}\left({X}\right)$
5 eqeq1 ${⊢}{y}={X}\to \left({y}={x}\mathrm{ball}\left({m}\right){r}↔{X}={x}\mathrm{ball}\left({m}\right){r}\right)$
6 5 rexbidv ${⊢}{y}={X}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}={x}\mathrm{ball}\left({m}\right){r}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}\right)$
7 6 raleqbi1dv ${⊢}{y}={X}\to \left(\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}={x}\mathrm{ball}\left({m}\right){r}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}\right)$
8 4 7 rabeqbidv ${⊢}{y}={X}\to \left\{{m}\in \mathrm{Met}\left({y}\right)|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}={x}\mathrm{ball}\left({m}\right){r}\right\}=\left\{{m}\in \mathrm{Met}\left({X}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}\right\}$
9 df-bnd ${⊢}\mathrm{Bnd}=\left({y}\in \mathrm{V}⟼\left\{{m}\in \mathrm{Met}\left({y}\right)|\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}={x}\mathrm{ball}\left({m}\right){r}\right\}\right)$
10 fvex ${⊢}\mathrm{Met}\left({X}\right)\in \mathrm{V}$
11 10 rabex ${⊢}\left\{{m}\in \mathrm{Met}\left({X}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}\right\}\in \mathrm{V}$
12 8 9 11 fvmpt ${⊢}{X}\in \mathrm{V}\to \mathrm{Bnd}\left({X}\right)=\left\{{m}\in \mathrm{Met}\left({X}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}\right\}$
13 12 eleq2d ${⊢}{X}\in \mathrm{V}\to \left({M}\in \mathrm{Bnd}\left({X}\right)↔{M}\in \left\{{m}\in \mathrm{Met}\left({X}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}\right\}\right)$
14 fveq2 ${⊢}{m}={M}\to \mathrm{ball}\left({m}\right)=\mathrm{ball}\left({M}\right)$
15 14 oveqd ${⊢}{m}={M}\to {x}\mathrm{ball}\left({m}\right){r}={x}\mathrm{ball}\left({M}\right){r}$
16 15 eqeq2d ${⊢}{m}={M}\to \left({X}={x}\mathrm{ball}\left({m}\right){r}↔{X}={x}\mathrm{ball}\left({M}\right){r}\right)$
17 16 rexbidv ${⊢}{m}={M}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$
18 17 ralbidv ${⊢}{m}={M}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$
19 18 elrab ${⊢}{M}\in \left\{{m}\in \mathrm{Met}\left({X}\right)|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({m}\right){r}\right\}↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$
20 13 19 syl6bb ${⊢}{X}\in \mathrm{V}\to \left({M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)$
21 1 3 20 pm5.21nii ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$