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 = ( 𝑥 ∈ V ↦ { 𝑚 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑥 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctotbnd	⊢ TotBnd
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vm	⊢ 𝑚
4		cmet	⊢ Met
5	1	cv	⊢ 𝑥
6	5 4	cfv	⊢ ( Met ‘ 𝑥 )
7		vd	⊢ 𝑑
8		crp	⊢ ℝ+
9		vv	⊢ 𝑣
10		cfn	⊢ Fin
11	9	cv	⊢ 𝑣
12	11	cuni	⊢ ∪ 𝑣
13	12 5	wceq	⊢ ∪ 𝑣 = 𝑥
14		vb	⊢ 𝑏
15		vy	⊢ 𝑦
16	14	cv	⊢ 𝑏
17	15	cv	⊢ 𝑦
18		cbl	⊢ ball
19	3	cv	⊢ 𝑚
20	19 18	cfv	⊢ ( ball ‘ 𝑚 )
21	7	cv	⊢ 𝑑
22	17 21 20	co	⊢ ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 )
23	16 22	wceq	⊢ 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 )
24	23 15 5	wrex	⊢ ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 )
25	24 14 11	wral	⊢ ∀ 𝑏 ∈ 𝑣 ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 )
26	13 25	wa	⊢ ( ∪ 𝑣 = 𝑥 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 ) )
27	26 9 10	wrex	⊢ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑥 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 ) )
28	27 7 8	wral	⊢ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑥 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 ) )
29	28 3 6	crab	⊢ { 𝑚 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑥 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 ) ) }
30	1 2 29	cmpt	⊢ ( 𝑥 ∈ V ↦ { 𝑚 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑥 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 ) ) } )
31	0 30	wceq	⊢ TotBnd = ( 𝑥 ∈ V ↦ { 𝑚 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑥 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑦 ∈ 𝑥 𝑏 = ( 𝑦 ( ball ‘ 𝑚 ) 𝑑 ) ) } )