Step | Hyp | Ref
| Expression |
1 | | df-metid 32460 |
. 2
⊢
~Met = (𝑑
∈ ∪ ran PsMet ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}) |
2 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
3 | 2 | dmeqd 5861 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom 𝑑 = dom 𝐷) |
4 | 3 | dmeqd 5861 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = dom dom 𝐷) |
5 | | psmetdmdm 23656 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
6 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑋 = dom dom 𝐷) |
7 | 4, 6 | eqtr4d 2779 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋) |
8 | 7 | eleq2d 2823 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥 ∈ dom dom 𝑑 ↔ 𝑥 ∈ 𝑋)) |
9 | 7 | eleq2d 2823 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑦 ∈ dom dom 𝑑 ↔ 𝑦 ∈ 𝑋)) |
10 | 8, 9 | anbi12d 631 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
11 | 2 | oveqd 7373 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥𝑑𝑦) = (𝑥𝐷𝑦)) |
12 | 11 | eqeq1d 2738 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥𝑑𝑦) = 0 ↔ (𝑥𝐷𝑦) = 0)) |
13 | 10, 12 | anbi12d 631 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0))) |
14 | 13 | opabbidv 5171 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) |
15 | | elfvunirn 6874 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ ∪ ran
PsMet) |
16 | | opabssxp 5724 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)} ⊆ (𝑋 × 𝑋) |
17 | | elfvex 6880 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ V) |
18 | 17, 17 | xpexd 7684 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑋 × 𝑋) ∈ V) |
19 | | ssexg 5280 |
. . 3
⊢
(({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)} ⊆ (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ V) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)} ∈ V) |
20 | 16, 18, 19 | sylancr 587 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)} ∈ V) |
21 | 1, 14, 15, 20 | fvmptd2 6956 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷) =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) |