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
|
syl6bb |
⊢ ( 𝑋 ∈ V → ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ) |
21 |
1 3 20
|
pm5.21nii |
⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) |