Definition df-totbnd 32737

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 32735	. 2 class TotBnd
2		vx	. . 3 setvar 𝑥
3		cvv 3173	. . 3 class V
4		vv	. . . . . . . . . 10 setvar 𝑣
5	4	cv 1474	. . . . . . . . 9 class 𝑣
6	5	cuni 4372	. . . . . . . 8 class ∪ 𝑣
7	2	cv 1474	. . . . . . . 8 class 𝑥
8	6, 7	wceq 1475	. . . . . . 7 wff ∪ 𝑣 = 𝑥
9		vb	. . . . . . . . . . 11 setvar 𝑏
10	9	cv 1474	. . . . . . . . . 10 class 𝑏
11		vy	. . . . . . . . . . . 12 setvar 𝑦
12	11	cv 1474	. . . . . . . . . . 11 class 𝑦
13		vd	. . . . . . . . . . . 12 setvar 𝑑
14	13	cv 1474	. . . . . . . . . . 11 class 𝑑
15		vm	. . . . . . . . . . . . 13 setvar 𝑚
16	15	cv 1474	. . . . . . . . . . . 12 class 𝑚
17		cbl 19554	. . . . . . . . . . . 12 class ball
18	16, 17	cfv 5804	. . . . . . . . . . 11 class (ball‘𝑚)
19	12, 14, 18	co 6549	. . . . . . . . . 10 class (𝑦(ball‘𝑚)𝑑)
20	10, 19	wceq 1475	. . . . . . . . 9 wff 𝑏 = (𝑦(ball‘𝑚)𝑑)
21	20, 11, 7	wrex 2897	. . . . . . . 8 wff ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑)
22	21, 9, 5	wral 2896	. . . . . . 7 wff ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑)
23	8, 22	wa 383	. . . . . 6 wff (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
24		cfn 7841	. . . . . 6 class Fin
25	23, 4, 24	wrex 2897	. . . . 5 wff ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
26		crp 11708	. . . . 5 class ℝ+
27	25, 13, 26	wral 2896	. . . 4 wff ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))
28		cme 19553	. . . . 5 class Met
29	7, 28	cfv 5804	. . . 4 class (Met‘𝑥)
30	27, 15, 29	crab 2900	. . 3 class {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))}
31	2, 3, 30	cmpt 4643	. 2 class (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})
32	1, 31	wceq 1475	1 wff TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})

This definition is referenced by:  istotbnd  32738