Definition df-totbnd 37775

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.)

Assertion

Ref	Expression
df-totbnd	⊢ TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})

Distinct variable group:   𝑏,𝑑,𝑚,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-totbnd

Step	Hyp	Ref	Expression
1		ctotbnd 37773	. 2 class TotBnd
2		vx	. . 3 setvar 𝑥
3		cvv 3480	. . 3 class V
4		vv	. . . . . . . . . 10 setvar 𝑣
5	4	cv 1539	. . . . . . . . 9 class 𝑣
6	5	cuni 4907	. . . . . . . 8 class ∪ 𝑣
7	2	cv 1539	. . . . . . . 8 class 𝑥
8	6, 7	wceq 1540	. . . . . . 7 wff ∪ 𝑣 = 𝑥
9		vb	. . . . . . . . . . 11 setvar 𝑏
10	9	cv 1539	. . . . . . . . . 10 class 𝑏
11		vy	. . . . . . . . . . . 12 setvar 𝑦
12	11	cv 1539	. . . . . . . . . . 11 class 𝑦
13		vd	. . . . . . . . . . . 12 setvar 𝑑
14	13	cv 1539	. . . . . . . . . . 11 class 𝑑
15		vm	. . . . . . . . . . . . 13 setvar 𝑚
16	15	cv 1539	. . . . . . . . . . . 12 class 𝑚
17		cbl 21351	. . . . . . . . . . . 12 class ball
18	16, 17	cfv 6561	. . . . . . . . . . 11 class (ball‘𝑚)
19	12, 14, 18	co 7431	. . . . . . . . . 10 class (𝑦(ball‘𝑚)𝑑)
20	10, 19	wceq 1540	. . . . . . . . 9 wff 𝑏 = (𝑦(ball‘𝑚)𝑑)
21	20, 11, 7	wrex 3070	. . . . . . . 8 wff ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑)
22	21, 9, 5	wral 3061	. . . . . . 7 wff ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑)
23	8, 22	wa 395	. . . . . 6 wff (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
24		cfn 8985	. . . . . 6 class Fin
25	23, 4, 24	wrex 3070	. . . . 5 wff ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
26		crp 13034	. . . . 5 class ℝ+
27	25, 13, 26	wral 3061	. . . 4 wff ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
28		cmet 21350	. . . . 5 class Met
29	7, 28	cfv 6561	. . . 4 class (Met‘𝑥)
30	27, 15, 29	crab 3436	. . 3 class {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))}
31	2, 3, 30	cmpt 5225	. 2 class (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})
32	1, 31	wceq 1540	1 wff TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})

This definition is referenced by:  istotbnd  37776