| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfvex 6943 | . 2
⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑋 ∈ V) | 
| 2 |  | elfvex 6943 | . . 3
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑋 ∈ V) | 
| 3 | 2 | adantr 480 | . 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)) → 𝑋 ∈ V) | 
| 4 |  | fveq2 6905 | . . . . . 6
⊢ (𝑦 = 𝑋 → (Met‘𝑦) = (Met‘𝑋)) | 
| 5 |  | eqeq1 2740 | . . . . . . . 8
⊢ (𝑦 = 𝑋 → (𝑦 = (𝑥(ball‘𝑚)𝑟) ↔ 𝑋 = (𝑥(ball‘𝑚)𝑟))) | 
| 6 | 5 | rexbidv 3178 | . . . . . . 7
⊢ (𝑦 = 𝑋 → (∃𝑟 ∈ ℝ+ 𝑦 = (𝑥(ball‘𝑚)𝑟) ↔ ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟))) | 
| 7 | 6 | raleqbi1dv 3337 | . . . . . 6
⊢ (𝑦 = 𝑋 → (∀𝑥 ∈ 𝑦 ∃𝑟 ∈ ℝ+ 𝑦 = (𝑥(ball‘𝑚)𝑟) ↔ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟))) | 
| 8 | 4, 7 | rabeqbidv 3454 | . . . . 5
⊢ (𝑦 = 𝑋 → {𝑚 ∈ (Met‘𝑦) ∣ ∀𝑥 ∈ 𝑦 ∃𝑟 ∈ ℝ+ 𝑦 = (𝑥(ball‘𝑚)𝑟)} = {𝑚 ∈ (Met‘𝑋) ∣ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟)}) | 
| 9 |  | df-bnd 37787 | . . . . 5
⊢ Bnd =
(𝑦 ∈ V ↦ {𝑚 ∈ (Met‘𝑦) ∣ ∀𝑥 ∈ 𝑦 ∃𝑟 ∈ ℝ+ 𝑦 = (𝑥(ball‘𝑚)𝑟)}) | 
| 10 |  | fvex 6918 | . . . . . 6
⊢
(Met‘𝑋) ∈
V | 
| 11 | 10 | rabex 5338 | . . . . 5
⊢ {𝑚 ∈ (Met‘𝑋) ∣ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟)} ∈ V | 
| 12 | 8, 9, 11 | fvmpt 7015 | . . . 4
⊢ (𝑋 ∈ V →
(Bnd‘𝑋) = {𝑚 ∈ (Met‘𝑋) ∣ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟)}) | 
| 13 | 12 | eleq2d 2826 | . . 3
⊢ (𝑋 ∈ V → (𝑀 ∈ (Bnd‘𝑋) ↔ 𝑀 ∈ {𝑚 ∈ (Met‘𝑋) ∣ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟)})) | 
| 14 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑚 = 𝑀 → (ball‘𝑚) = (ball‘𝑀)) | 
| 15 | 14 | oveqd 7449 | . . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑥(ball‘𝑚)𝑟) = (𝑥(ball‘𝑀)𝑟)) | 
| 16 | 15 | eqeq2d 2747 | . . . . . 6
⊢ (𝑚 = 𝑀 → (𝑋 = (𝑥(ball‘𝑚)𝑟) ↔ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | 
| 17 | 16 | rexbidv 3178 | . . . . 5
⊢ (𝑚 = 𝑀 → (∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟) ↔ ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | 
| 18 | 17 | ralbidv 3177 | . . . 4
⊢ (𝑚 = 𝑀 → (∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟) ↔ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | 
| 19 | 18 | elrab 3691 | . . 3
⊢ (𝑀 ∈ {𝑚 ∈ (Met‘𝑋) ∣ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑚)𝑟)} ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | 
| 20 | 13, 19 | bitrdi 287 | . 2
⊢ (𝑋 ∈ V → (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)))) | 
| 21 | 1, 3, 20 | pm5.21nii 378 | 1
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |