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 ∈ x b = y ball ⁡ m d

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctotbnd class TotBnd
1 vx setvar x
2 cvv class V
3 vm setvar m
4 cmet class Met
5 1 cv setvar x
6 5 4 cfv class Met ⁡ x
7 vd setvar d
8 crp class ℝ +
9 vv setvar v
10 cfn class Fin
11 9 cv setvar v
12 11 cuni class ⋃ v
13 12 5 wceq wff ⋃ v = x
14 vb setvar b
15 vy setvar y
16 14 cv setvar b
17 15 cv setvar y
18 cbl class ball
19 3 cv setvar m
20 19 18 cfv class ball ⁡ m
21 7 cv setvar d
22 17 21 20 co class y ball ⁡ m d
23 16 22 wceq wff b = y ball ⁡ m d
24 23 15 5 wrex wff ∃ y ∈ x b = y ball ⁡ m d
25 24 14 11 wral wff ∀ b ∈ v ∃ y ∈ x b = y ball ⁡ m d
26 13 25 wa wff ⋃ v = x ∧ ∀ b ∈ v ∃ y ∈ x b = y ball ⁡ m d
27 26 9 10 wrex wff ∃ v ∈ Fin ⋃ v = x ∧ ∀ b ∈ v ∃ y ∈ x b = y ball ⁡ m d
28 27 7 8 wral wff ∀ d ∈ ℝ + ∃ v ∈ Fin ⋃ v = x ∧ ∀ b ∈ v ∃ y ∈ x b = y ball ⁡ m d
29 28 3 6 crab class m ∈ Met ⁡ x | ∀ d ∈ ℝ + ∃ v ∈ Fin ⋃ v = x ∧ ∀ b ∈ v ∃ y ∈ x b = y ball ⁡ m d
30 1 2 29 cmpt class x ∈ V ⟼ m ∈ Met ⁡ x | ∀ d ∈ ℝ + ∃ v ∈ Fin ⋃ v = x ∧ ∀ b ∈ v ∃ y ∈ x b = y ball ⁡ m d
31 0 30 wceq wff TotBnd = x ∈ V ⟼ m ∈ Met ⁡ x | ∀ d ∈ ℝ + ∃ v ∈ Fin ⋃ v = x ∧ ∀ b ∈ v ∃ y ∈ x b = y ball ⁡ m d