Detailed syntax breakdown of Definition df-xmet
Step | Hyp | Ref
| Expression |
1 | | cxmet 20580 |
. 2
class
∞Met |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
5 | 4 | cv 1541 |
. . . . . . . . . 10
class 𝑦 |
6 | | vz |
. . . . . . . . . . 11
setvar 𝑧 |
7 | 6 | cv 1541 |
. . . . . . . . . 10
class 𝑧 |
8 | | vd |
. . . . . . . . . . 11
setvar 𝑑 |
9 | 8 | cv 1541 |
. . . . . . . . . 10
class 𝑑 |
10 | 5, 7, 9 | co 7271 |
. . . . . . . . 9
class (𝑦𝑑𝑧) |
11 | | cc0 10872 |
. . . . . . . . 9
class
0 |
12 | 10, 11 | wceq 1542 |
. . . . . . . 8
wff (𝑦𝑑𝑧) = 0 |
13 | 4, 6 | weq 1970 |
. . . . . . . 8
wff 𝑦 = 𝑧 |
14 | 12, 13 | wb 205 |
. . . . . . 7
wff ((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) |
15 | | vw |
. . . . . . . . . . . 12
setvar 𝑤 |
16 | 15 | cv 1541 |
. . . . . . . . . . 11
class 𝑤 |
17 | 16, 5, 9 | co 7271 |
. . . . . . . . . 10
class (𝑤𝑑𝑦) |
18 | 16, 7, 9 | co 7271 |
. . . . . . . . . 10
class (𝑤𝑑𝑧) |
19 | | cxad 12845 |
. . . . . . . . . 10
class
+𝑒 |
20 | 17, 18, 19 | co 7271 |
. . . . . . . . 9
class ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)) |
21 | | cle 11011 |
. . . . . . . . 9
class
≤ |
22 | 10, 20, 21 | wbr 5079 |
. . . . . . . 8
wff (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)) |
23 | 2 | cv 1541 |
. . . . . . . 8
class 𝑥 |
24 | 22, 15, 23 | wral 3066 |
. . . . . . 7
wff
∀𝑤 ∈
𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)) |
25 | 14, 24 | wa 396 |
. . . . . 6
wff (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))) |
26 | 25, 6, 23 | wral 3066 |
. . . . 5
wff
∀𝑧 ∈
𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))) |
27 | 26, 4, 23 | wral 3066 |
. . . 4
wff
∀𝑦 ∈
𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))) |
28 | | cxr 11009 |
. . . . 5
class
ℝ* |
29 | 23, 23 | cxp 5588 |
. . . . 5
class (𝑥 × 𝑥) |
30 | | cmap 8598 |
. . . . 5
class
↑m |
31 | 28, 29, 30 | co 7271 |
. . . 4
class
(ℝ* ↑m (𝑥 × 𝑥)) |
32 | 27, 8, 31 | crab 3070 |
. . 3
class {𝑑 ∈ (ℝ*
↑m (𝑥
× 𝑥)) ∣
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))} |
33 | 2, 3, 32 | cmpt 5162 |
. 2
class (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*
↑m (𝑥
× 𝑥)) ∣
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) |
34 | 1, 33 | wceq 1542 |
1
wff ∞Met
= (𝑥 ∈ V ↦
{𝑑 ∈
(ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) |