Detailed syntax breakdown of Definition df-metid
Step | Hyp | Ref
| Expression |
1 | | cmetid 31823 |
. 2
class
~Met |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cpsmet 20570 |
. . . . 5
class
PsMet |
4 | 3 | crn 5587 |
. . . 4
class ran
PsMet |
5 | 4 | cuni 4841 |
. . 3
class ∪ ran PsMet |
6 | | vx |
. . . . . . . 8
setvar 𝑥 |
7 | 6 | cv 1538 |
. . . . . . 7
class 𝑥 |
8 | 2 | cv 1538 |
. . . . . . . . 9
class 𝑑 |
9 | 8 | cdm 5586 |
. . . . . . . 8
class dom 𝑑 |
10 | 9 | cdm 5586 |
. . . . . . 7
class dom dom
𝑑 |
11 | 7, 10 | wcel 2106 |
. . . . . 6
wff 𝑥 ∈ dom dom 𝑑 |
12 | | vy |
. . . . . . . 8
setvar 𝑦 |
13 | 12 | cv 1538 |
. . . . . . 7
class 𝑦 |
14 | 13, 10 | wcel 2106 |
. . . . . 6
wff 𝑦 ∈ dom dom 𝑑 |
15 | 11, 14 | wa 396 |
. . . . 5
wff (𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) |
16 | 7, 13, 8 | co 7269 |
. . . . . 6
class (𝑥𝑑𝑦) |
17 | | cc0 10860 |
. . . . . 6
class
0 |
18 | 16, 17 | wceq 1539 |
. . . . 5
wff (𝑥𝑑𝑦) = 0 |
19 | 15, 18 | wa 396 |
. . . 4
wff ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0) |
20 | 19, 6, 12 | copab 5137 |
. . 3
class
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)} |
21 | 2, 5, 20 | cmpt 5158 |
. 2
class (𝑑 ∈ ∪ ran PsMet ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}) |
22 | 1, 21 | wceq 1539 |
1
wff
~Met = (𝑑
∈ ∪ ran PsMet ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}) |