Detailed syntax breakdown of Definition df-bl
Step | Hyp | Ref
| Expression |
1 | | cbl 20204 |
. 2
class
ball |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cvv 3398 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | | vz |
. . . 4
setvar 𝑧 |
6 | 2 | cv 1541 |
. . . . . 6
class 𝑑 |
7 | 6 | cdm 5525 |
. . . . 5
class dom 𝑑 |
8 | 7 | cdm 5525 |
. . . 4
class dom dom
𝑑 |
9 | | cxr 10752 |
. . . 4
class
ℝ* |
10 | 4 | cv 1541 |
. . . . . . 7
class 𝑥 |
11 | | vy |
. . . . . . . 8
setvar 𝑦 |
12 | 11 | cv 1541 |
. . . . . . 7
class 𝑦 |
13 | 10, 12, 6 | co 7170 |
. . . . . 6
class (𝑥𝑑𝑦) |
14 | 5 | cv 1541 |
. . . . . 6
class 𝑧 |
15 | | clt 10753 |
. . . . . 6
class
< |
16 | 13, 14, 15 | wbr 5030 |
. . . . 5
wff (𝑥𝑑𝑦) < 𝑧 |
17 | 16, 11, 8 | crab 3057 |
. . . 4
class {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧} |
18 | 4, 5, 8, 9, 17 | cmpo 7172 |
. . 3
class (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}) |
19 | 2, 3, 18 | cmpt 5110 |
. 2
class (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧})) |
20 | 1, 19 | wceq 1542 |
1
wff ball =
(𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧})) |