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 ⊢TotBnd=x∈V⟼m∈Met⁡x|∀d∈ℝ+∃v∈Fin⋃v=x∧∀b∈v∃y∈xb=yball⁡md

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctotbnd classTotBnd
1 vx setvarx
2 cvv classV
3 vm setvarm
4 cmet classMet
5 1 cv setvarx
6 5 4 cfv classMet⁡x
7 vd setvard
8 crp classℝ+
9 vv setvarv
10 cfn classFin
11 9 cv setvarv
12 11 cuni class⋃v
13 12 5 wceq wff⋃v=x
14 vb setvarb
15 vy setvary
16 14 cv setvarb
17 15 cv setvary
18 cbl classball
19 3 cv setvarm
20 19 18 cfv classball⁡m
21 7 cv setvard
22 17 21 20 co classyball⁡md
23 16 22 wceq wffb=yball⁡md
24 23 15 5 wrex wff∃y∈xb=yball⁡md
25 24 14 11 wral wff∀b∈v∃y∈xb=yball⁡md
26 13 25 wa wff⋃v=x∧∀b∈v∃y∈xb=yball⁡md
27 26 9 10 wrex wff∃v∈Fin⋃v=x∧∀b∈v∃y∈xb=yball⁡md
28 27 7 8 wral wff∀d∈ℝ+∃v∈Fin⋃v=x∧∀b∈v∃y∈xb=yball⁡md
29 28 3 6 crab classm∈Met⁡x|∀d∈ℝ+∃v∈Fin⋃v=x∧∀b∈v∃y∈xb=yball⁡md
30 1 2 29 cmpt classx∈V⟼m∈Met⁡x|∀d∈ℝ+∃v∈Fin⋃v=x∧∀b∈v∃y∈xb=yball⁡md
31 0 30 wceq wffTotBnd=x∈V⟼m∈Met⁡x|∀d∈ℝ+∃v∈Fin⋃v=x∧∀b∈v∃y∈xb=yball⁡md