# Metamath Proof Explorer

## Definition df-totbnd

Description: Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion df-totbnd ${⊢}\mathrm{TotBnd}=\left({x}\in \mathrm{V}⟼\left\{{m}\in \mathrm{Met}\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 {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ctotbnd ${class}\mathrm{TotBnd}$
1 vx ${setvar}{x}$
2 cvv ${class}\mathrm{V}$
3 vm ${setvar}{m}$
4 cmet ${class}\mathrm{Met}$
5 1 cv ${setvar}{x}$
6 5 4 cfv ${class}\mathrm{Met}\left({x}\right)$
7 vd ${setvar}{d}$
8 crp ${class}{ℝ}^{+}$
9 vv ${setvar}{v}$
10 cfn ${class}\mathrm{Fin}$
11 9 cv ${setvar}{v}$
12 11 cuni ${class}\bigcup {v}$
13 12 5 wceq ${wff}\bigcup {v}={x}$
14 vb ${setvar}{b}$
15 vy ${setvar}{y}$
16 14 cv ${setvar}{b}$
17 15 cv ${setvar}{y}$
18 cbl ${class}\mathrm{ball}$
19 3 cv ${setvar}{m}$
20 19 18 cfv ${class}\mathrm{ball}\left({m}\right)$
21 7 cv ${setvar}{d}$
22 17 21 20 co ${class}\left({y}\mathrm{ball}\left({m}\right){d}\right)$
23 16 22 wceq ${wff}{b}={y}\mathrm{ball}\left({m}\right){d}$
24 23 15 5 wrex ${wff}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}$
25 24 14 11 wral ${wff}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}$
26 13 25 wa ${wff}\left(\bigcup {v}={x}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}\right)$
27 26 9 10 wrex ${wff}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {v}={x}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}\right)$
28 27 7 8 wral ${wff}\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 {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}\right)$
29 28 3 6 crab ${class}\left\{{m}\in \mathrm{Met}\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 {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}\right)\right\}$
30 1 2 29 cmpt ${class}\left({x}\in \mathrm{V}⟼\left\{{m}\in \mathrm{Met}\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 {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}\right)\right\}\right)$
31 0 30 wceq ${wff}\mathrm{TotBnd}=\left({x}\in \mathrm{V}⟼\left\{{m}\in \mathrm{Met}\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 {y}\in {x}\phantom{\rule{.4em}{0ex}}{b}={y}\mathrm{ball}\left({m}\right){d}\right)\right\}\right)$