This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑀 ) 𝑑 ) ) ) )