Detailed syntax breakdown of Definition df-ico
Step | Hyp | Ref
| Expression |
1 | | cico 9847 |
. 2
class
[,) |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cxr 7953 |
. . 3
class
ℝ* |
5 | 2 | cv 1347 |
. . . . . 6
class 𝑥 |
6 | | vz |
. . . . . . 7
setvar 𝑧 |
7 | 6 | cv 1347 |
. . . . . 6
class 𝑧 |
8 | | cle 7955 |
. . . . . 6
class
≤ |
9 | 5, 7, 8 | wbr 3989 |
. . . . 5
wff 𝑥 ≤ 𝑧 |
10 | 3 | cv 1347 |
. . . . . 6
class 𝑦 |
11 | | clt 7954 |
. . . . . 6
class
< |
12 | 7, 10, 11 | wbr 3989 |
. . . . 5
wff 𝑧 < 𝑦 |
13 | 9, 12 | wa 103 |
. . . 4
wff (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦) |
14 | 13, 6, 4 | crab 2452 |
. . 3
class {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} |
15 | 2, 3, 4, 4, 14 | cmpo 5855 |
. 2
class (𝑥 ∈ ℝ*,
𝑦 ∈
ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
16 | 1, 15 | wceq 1348 |
1
wff [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |