Theorem istotbnd

Description: The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	istotbnd	⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → 𝑋 ∈ V )
2		elfvex	⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑋 ∈ V )
3	2	adantr	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑋 ∈ V )
4		fveq2	⊢ ( 𝑦 = 𝑋 → ( Met ‘ 𝑦 ) = ( Met ‘ 𝑋 ) )
5		eqeq2	⊢ ( 𝑦 = 𝑋 → ( ∪ 𝑣 = 𝑦 ↔ ∪ 𝑣 = 𝑋 ) )
6		rexeq	⊢ ( 𝑦 = 𝑋 → ( ∃ 𝑥 ∈ 𝑦 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ↔ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) )
7	6	ralbidv	⊢ ( 𝑦 = 𝑋 → ( ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑦 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ↔ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) )
8	5 7	anbi12d	⊢ ( 𝑦 = 𝑋 → ( ( ∪ 𝑣 = 𝑦 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑦 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ↔ ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ) )
9	8	rexbidv	⊢ ( 𝑦 = 𝑋 → ( ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑦 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑦 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ↔ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ) )
10	9	ralbidv	⊢ ( 𝑦 = 𝑋 → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑦 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑦 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ) )
11	4 10	rabeqbidv	⊢ ( 𝑦 = 𝑋 → { 𝑚 ∈ ( Met ‘ 𝑦 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑦 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑦 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) } = { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) } )
12		df-totbnd	⊢ TotBnd = ( 𝑦 ∈ V ↦ { 𝑚 ∈ ( Met ‘ 𝑦 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑦 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑦 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) } )
13		fvex	⊢ ( Met ‘ 𝑋 ) ∈ V
14	13	rabex	⊢ { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) } ∈ V
15	11 12 14	fvmpt	⊢ ( 𝑋 ∈ V → ( TotBnd ‘ 𝑋 ) = { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) } )
16	15	eleq2d	⊢ ( 𝑋 ∈ V → ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ 𝑀 ∈ { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) } ) )
17		fveq2	⊢ ( 𝑚 = 𝑀 → ( ball ‘ 𝑚 ) = ( ball ‘ 𝑀 ) )
18	17	oveqd	⊢ ( 𝑚 = 𝑀 → ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
19	18	eqeq2d	⊢ ( 𝑚 = 𝑀 → ( 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ↔ 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
20	19	rexbidv	⊢ ( 𝑚 = 𝑀 → ( ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ↔ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
21	20	ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ↔ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
22	21	anbi2d	⊢ ( 𝑚 = 𝑀 → ( ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ↔ ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
23	22	rexbidv	⊢ ( 𝑚 = 𝑀 → ( ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ↔ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
24	23	ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
25	24	elrab	⊢ ( 𝑀 ∈ { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑑 ) ) } ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
26	16 25	bitrdi	⊢ ( 𝑋 ∈ V → ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) )
27	1 3 26	pm5.21nii	⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( ∪ 𝑣 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )