Step | Hyp | Ref
| Expression |
1 | | df-metid 29259 |
. . 3
⊢
~Met = (𝑑
∈ ∪ ran PsMet ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → ~Met =
(𝑑 ∈ ∪ ran PsMet ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})) |
3 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
4 | 3 | dmeqd 5248 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom 𝑑 = dom 𝐷) |
5 | 4 | dmeqd 5248 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = dom dom 𝐷) |
6 | | psmetdmdm 21920 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑋 = dom dom 𝐷) |
8 | 5, 7 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋) |
9 | 8 | eleq2d 2673 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥 ∈ dom dom 𝑑 ↔ 𝑥 ∈ 𝑋)) |
10 | 8 | eleq2d 2673 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑦 ∈ dom dom 𝑑 ↔ 𝑦 ∈ 𝑋)) |
11 | 9, 10 | anbi12d 743 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
12 | 3 | oveqd 6566 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥𝑑𝑦) = (𝑥𝐷𝑦)) |
13 | 12 | eqeq1d 2612 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥𝑑𝑦) = 0 ↔ (𝑥𝐷𝑦) = 0)) |
14 | 11, 13 | anbi12d 743 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0))) |
15 | 14 | opabbidv 4648 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) |
16 | | elfvdm 6130 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet) |
17 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (PsMet‘𝑥) = (PsMet‘𝑋)) |
18 | 17 | eleq2d 2673 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐷 ∈ (PsMet‘𝑥) ↔ 𝐷 ∈ (PsMet‘𝑋))) |
19 | 18 | rspcev 3282 |
. . . 4
⊢ ((𝑋 ∈ dom PsMet ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
20 | 16, 19 | mpancom 700 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
21 | | df-psmet 19559 |
. . . . 5
⊢ PsMet =
(𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*
↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) |
22 | 21 | funmpt2 5841 |
. . . 4
⊢ Fun
PsMet |
23 | | elunirn 6413 |
. . . 4
⊢ (Fun
PsMet → (𝐷 ∈
∪ ran PsMet ↔ ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥))) |
24 | 22, 23 | ax-mp 5 |
. . 3
⊢ (𝐷 ∈ ∪ ran PsMet ↔ ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
25 | 20, 24 | sylibr 223 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ ∪ ran
PsMet) |
26 | | opabssxp 5116 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)} ⊆ (𝑋 × 𝑋) |
27 | | elfvex 6131 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ V) |
28 | | xpexg 6858 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝑋 ∈ V) → (𝑋 × 𝑋) ∈ V) |
29 | 27, 27, 28 | syl2anc 691 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑋 × 𝑋) ∈ V) |
30 | | ssexg 4732 |
. . 3
⊢
(({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)} ⊆ (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ V) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)} ∈ V) |
31 | 26, 29, 30 | sylancr 694 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)} ∈ V) |
32 | 2, 15, 25, 31 | fvmptd 6197 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷) =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) |