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