Step | Hyp | Ref
| Expression |
1 | | df-bl 19562 |
. . 3
⊢ ball =
(𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟})) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}))) |
3 | | dmeq 5246 |
. . . . 5
⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷) |
4 | 3 | dmeqd 5248 |
. . . 4
⊢ (𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷) |
5 | | psmetdmdm 21920 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
6 | 5 | eqcomd 2616 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom dom 𝐷 = 𝑋) |
7 | 4, 6 | sylan9eqr 2666 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋) |
8 | | eqidd 2611 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ℝ* =
ℝ*) |
9 | | simpr 476 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
10 | 9 | oveqd 6566 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥𝑑𝑦) = (𝑥𝐷𝑦)) |
11 | 10 | breq1d 4593 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥𝑑𝑦) < 𝑟 ↔ (𝑥𝐷𝑦) < 𝑟)) |
12 | 7, 11 | rabeqbidv 3168 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟} = {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) |
13 | 7, 8, 12 | mpt2eq123dv 6615 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) |
14 | | elex 3185 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ V) |
15 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋 |
16 | | elfvdm 6130 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → 𝑋 ∈ dom
PsMet) |
18 | | elpw2g 4754 |
. . . . . . 7
⊢ (𝑋 ∈ dom PsMet → ({𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋)) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → ({𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋)) |
20 | 15, 19 | mpbiri 247 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋) |
21 | 20 | ralrimivva 2954 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ* {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋) |
22 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) |
23 | 22 | fmpt2 7126 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑟 ∈ ℝ*
{𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
24 | 21, 23 | sylib 207 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
25 | | xrex 11705 |
. . . 4
⊢
ℝ* ∈ V |
26 | | xpexg 6858 |
. . . 4
⊢ ((𝑋 ∈ dom PsMet ∧
ℝ* ∈ V) → (𝑋 × ℝ*) ∈
V) |
27 | 16, 25, 26 | sylancl 693 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑋 × ℝ*) ∈
V) |
28 | | pwexg 4776 |
. . . 4
⊢ (𝑋 ∈ dom PsMet →
𝒫 𝑋 ∈
V) |
29 | 16, 28 | syl 17 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝒫 𝑋 ∈ V) |
30 | | fex2 7014 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋 ∧ (𝑋 × ℝ*) ∈ V ∧
𝒫 𝑋 ∈ V)
→ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V) |
31 | 24, 27, 29, 30 | syl3anc 1318 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V) |
32 | 2, 13, 14, 31 | fvmptd 6197 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) |