Metamath Proof Explorer

Theorem isbnd

Description: The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion isbnd ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) → 𝑋 ∈ V )
2 elfvex ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑋 ∈ V )
3 2 adantr ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → 𝑋 ∈ V )
4 fveq2 ⊢ ( 𝑦 = 𝑋 → ( Met ‘ 𝑦 ) = ( Met ‘ 𝑋 ) )
5 eqeq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ↔ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ) )
6 5 rexbidv ⊢ ( 𝑦 = 𝑋 → ( ∃ 𝑟 ∈ ℝ+ 𝑦 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ↔ ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ) )
7 6 raleqbi1dv ⊢ ( 𝑦 = 𝑋 → ( ∀ 𝑥 ∈ 𝑦 ∃ 𝑟 ∈ ℝ+ 𝑦 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ) )
8 4 7 rabeqbidv ⊢ ( 𝑦 = 𝑋 → { 𝑚 ∈ ( Met ‘ 𝑦 ) ∣ ∀ 𝑥 ∈ 𝑦 ∃ 𝑟 ∈ ℝ+ 𝑦 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) } = { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) } )
9 df-bnd ⊢ Bnd = ( 𝑦 ∈ V ↦ { 𝑚 ∈ ( Met ‘ 𝑦 ) ∣ ∀ 𝑥 ∈ 𝑦 ∃ 𝑟 ∈ ℝ+ 𝑦 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) } )
10 fvex ⊢ ( Met ‘ 𝑋 ) ∈ V
11 10 rabex ⊢ { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) } ∈ V
12 8 9 11 fvmpt ⊢ ( 𝑋 ∈ V → ( Bnd ‘ 𝑋 ) = { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) } )
13 12 eleq2d ⊢ ( 𝑋 ∈ V → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ 𝑀 ∈ { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) } ) )
14 fveq2 ⊢ ( 𝑚 = 𝑀 → ( ball ‘ 𝑚 ) = ( ball ‘ 𝑀 ) )
15 14 oveqd ⊢ ( 𝑚 = 𝑀 → ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
16 15 eqeq2d ⊢ ( 𝑚 = 𝑀 → ( 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ↔ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
17 16 rexbidv ⊢ ( 𝑚 = 𝑀 → ( ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ↔ ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
18 17 ralbidv ⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
19 18 elrab ⊢ ( 𝑀 ∈ { 𝑚 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑚 ) 𝑟 ) } ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
20 13 19 bitrdi ⊢ ( 𝑋 ∈ V → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) )
21 1 3 20 pm5.21nii ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )