# Metamath Proof Explorer

## Theorem istotbnd2

Description: The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion istotbnd2 ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left({M}\in \mathrm{TotBnd}\left({X}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {v}={X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$

### Proof

Step Hyp Ref Expression
1 istotbnd ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {v}={X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
2 1 baib ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left({M}\in \mathrm{TotBnd}\left({X}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {v}={X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$