Step | Hyp | Ref
| Expression |
1 | | df-bl 20137 |
. . 3
⊢ ball =
(𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟})) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}))) |
3 | | dmeq 5569 |
. . . . 5
⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷) |
4 | 3 | dmeqd 5571 |
. . . 4
⊢ (𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷) |
5 | | psmetdmdm 22518 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
6 | 5 | eqcomd 2784 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom dom 𝐷 = 𝑋) |
7 | 4, 6 | sylan9eqr 2836 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋) |
8 | | eqidd 2779 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ℝ* =
ℝ*) |
9 | | simpr 479 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
10 | 9 | oveqd 6939 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥𝑑𝑦) = (𝑥𝐷𝑦)) |
11 | 10 | breq1d 4896 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥𝑑𝑦) < 𝑟 ↔ (𝑥𝐷𝑦) < 𝑟)) |
12 | 7, 11 | rabeqbidv 3392 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟} = {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) |
13 | 7, 8, 12 | mpt2eq123dv 6994 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) |
14 | | elex 3414 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ V) |
15 | | ssrab2 3908 |
. . . . . 6
⊢ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋 |
16 | | elfvdm 6478 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet) |
17 | 16 | adantr 474 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → 𝑋 ∈ dom
PsMet) |
18 | | elpw2g 5061 |
. . . . . . 7
⊢ (𝑋 ∈ dom PsMet → ({𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋)) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → ({𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋)) |
20 | 15, 19 | mpbiri 250 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋) |
21 | 20 | ralrimivva 3153 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ* {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋) |
22 | | eqid 2778 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) |
23 | 22 | fmpt2 7517 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑟 ∈ ℝ*
{𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
24 | 21, 23 | sylib 210 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
25 | | xrex 12134 |
. . . 4
⊢
ℝ* ∈ V |
26 | | xpexg 7237 |
. . . 4
⊢ ((𝑋 ∈ dom PsMet ∧
ℝ* ∈ V) → (𝑋 × ℝ*) ∈
V) |
27 | 16, 25, 26 | sylancl 580 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑋 × ℝ*) ∈
V) |
28 | 16 | pwexd 5091 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝒫 𝑋 ∈ V) |
29 | | fex2 7400 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 ×
ℝ*)⟶𝒫 𝑋 ∧ (𝑋 × ℝ*) ∈ V ∧
𝒫 𝑋 ∈ V)
→ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V) |
30 | 24, 27, 28, 29 | syl3anc 1439 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V) |
31 | 2, 13, 14, 30 | fvmptd 6548 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) |