Step | Hyp | Ref
| Expression |
1 | | df-bl 20580 |
. 2
⊢ ball =
(𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟})) |
2 | | dmeq 5806 |
. . . . 5
⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷) |
3 | 2 | dmeqd 5808 |
. . . 4
⊢ (𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷) |
4 | | psmetdmdm 23446 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
5 | 4 | eqcomd 2744 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom dom 𝐷 = 𝑋) |
6 | 3, 5 | sylan9eqr 2800 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋) |
7 | | eqidd 2739 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ℝ* =
ℝ*) |
8 | | simpr 485 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
9 | 8 | oveqd 7285 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥𝑑𝑦) = (𝑥𝐷𝑦)) |
10 | 9 | breq1d 5084 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥𝑑𝑦) < 𝑟 ↔ (𝑥𝐷𝑦) < 𝑟)) |
11 | 6, 10 | rabeqbidv 3418 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟} = {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) |
12 | 6, 7, 11 | mpoeq123dv 7341 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) |
13 | | elex 3448 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ V) |
14 | | ssrab2 4013 |
. . . . . 6
⊢ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋 |
15 | | elfvdm 6799 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet) |
16 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → 𝑋 ∈ dom
PsMet) |
17 | | elpw2g 5267 |
. . . . . . 7
⊢ (𝑋 ∈ dom PsMet → ({𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → ({𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋)) |
19 | 14, 18 | mpbiri 257 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋) |
20 | 19 | ralrimivva 3120 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ* {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋) |
21 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) |
22 | 21 | fmpo 7898 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑟 ∈ ℝ*
{𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
23 | 20, 22 | sylib 217 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
24 | | xrex 12715 |
. . . 4
⊢
ℝ* ∈ V |
25 | | xpexg 7591 |
. . . 4
⊢ ((𝑋 ∈ dom PsMet ∧
ℝ* ∈ V) → (𝑋 × ℝ*) ∈
V) |
26 | 15, 24, 25 | sylancl 586 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑋 × ℝ*) ∈
V) |
27 | 15 | pwexd 5301 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝒫 𝑋 ∈ V) |
28 | | fex2 7771 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋 ∧ (𝑋 × ℝ*) ∈ V ∧
𝒫 𝑋 ∈ V)
→ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V) |
29 | 23, 26, 27, 28 | syl3anc 1370 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V) |
30 | 1, 12, 13, 29 | fvmptd2 6876 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) |