# Metamath Proof Explorer

## Definition df-bnd

Description: Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion df-bnd ${⊢}\mathrm{Bnd}=\left({x}\in \mathrm{V}⟼\left\{{m}\in \mathrm{Met}\left({x}\right)|\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{x}={y}\mathrm{ball}\left({m}\right){r}\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cbnd ${class}\mathrm{Bnd}$
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 vy ${setvar}{y}$
8 vr ${setvar}{r}$
9 crp ${class}{ℝ}^{+}$
10 7 cv ${setvar}{y}$
11 cbl ${class}\mathrm{ball}$
12 3 cv ${setvar}{m}$
13 12 11 cfv ${class}\mathrm{ball}\left({m}\right)$
14 8 cv ${setvar}{r}$
15 10 14 13 co ${class}\left({y}\mathrm{ball}\left({m}\right){r}\right)$
16 5 15 wceq ${wff}{x}={y}\mathrm{ball}\left({m}\right){r}$
17 16 8 9 wrex ${wff}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{x}={y}\mathrm{ball}\left({m}\right){r}$
18 17 7 5 wral ${wff}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{x}={y}\mathrm{ball}\left({m}\right){r}$
19 18 3 6 crab ${class}\left\{{m}\in \mathrm{Met}\left({x}\right)|\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{x}={y}\mathrm{ball}\left({m}\right){r}\right\}$
20 1 2 19 cmpt ${class}\left({x}\in \mathrm{V}⟼\left\{{m}\in \mathrm{Met}\left({x}\right)|\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{x}={y}\mathrm{ball}\left({m}\right){r}\right\}\right)$
21 0 20 wceq ${wff}\mathrm{Bnd}=\left({x}\in \mathrm{V}⟼\left\{{m}\in \mathrm{Met}\left({x}\right)|\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{x}={y}\mathrm{ball}\left({m}\right){r}\right\}\right)$