Detailed syntax breakdown of Definition df-met
Step | Hyp | Ref
| Expression |
1 | | cmet 20592 |
. 2
class
Met |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cvv 3433 |
. . 3
class
V |
4 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
5 | 4 | cv 1538 |
. . . . . . . . . 10
class 𝑦 |
6 | | vz |
. . . . . . . . . . 11
setvar 𝑧 |
7 | 6 | cv 1538 |
. . . . . . . . . 10
class 𝑧 |
8 | | vd |
. . . . . . . . . . 11
setvar 𝑑 |
9 | 8 | cv 1538 |
. . . . . . . . . 10
class 𝑑 |
10 | 5, 7, 9 | co 7284 |
. . . . . . . . 9
class (𝑦𝑑𝑧) |
11 | | cc0 10880 |
. . . . . . . . 9
class
0 |
12 | 10, 11 | wceq 1539 |
. . . . . . . 8
wff (𝑦𝑑𝑧) = 0 |
13 | 4, 6 | weq 1967 |
. . . . . . . 8
wff 𝑦 = 𝑧 |
14 | 12, 13 | wb 205 |
. . . . . . 7
wff ((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) |
15 | | vw |
. . . . . . . . . . . 12
setvar 𝑤 |
16 | 15 | cv 1538 |
. . . . . . . . . . 11
class 𝑤 |
17 | 16, 5, 9 | co 7284 |
. . . . . . . . . 10
class (𝑤𝑑𝑦) |
18 | 16, 7, 9 | co 7284 |
. . . . . . . . . 10
class (𝑤𝑑𝑧) |
19 | | caddc 10883 |
. . . . . . . . . 10
class
+ |
20 | 17, 18, 19 | co 7284 |
. . . . . . . . 9
class ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)) |
21 | | cle 11019 |
. . . . . . . . 9
class
≤ |
22 | 10, 20, 21 | wbr 5075 |
. . . . . . . 8
wff (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)) |
23 | 2 | cv 1538 |
. . . . . . . 8
class 𝑥 |
24 | 22, 15, 23 | wral 3065 |
. . . . . . 7
wff
∀𝑤 ∈
𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)) |
25 | 14, 24 | wa 396 |
. . . . . 6
wff (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧))) |
26 | 25, 6, 23 | wral 3065 |
. . . . 5
wff
∀𝑧 ∈
𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧))) |
27 | 26, 4, 23 | wral 3065 |
. . . 4
wff
∀𝑦 ∈
𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧))) |
28 | | cr 10879 |
. . . . 5
class
ℝ |
29 | 23, 23 | cxp 5588 |
. . . . 5
class (𝑥 × 𝑥) |
30 | | cmap 8624 |
. . . . 5
class
↑m |
31 | 28, 29, 30 | co 7284 |
. . . 4
class (ℝ
↑m (𝑥
× 𝑥)) |
32 | 27, 8, 31 | crab 3069 |
. . 3
class {𝑑 ∈ (ℝ
↑m (𝑥
× 𝑥)) ∣
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))} |
33 | 2, 3, 32 | cmpt 5158 |
. 2
class (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ
↑m (𝑥
× 𝑥)) ∣
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) |
34 | 1, 33 | wceq 1539 |
1
wff Met =
(𝑥 ∈ V ↦ {𝑑 ∈ (ℝ
↑m (𝑥
× 𝑥)) ∣
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) |