Detailed syntax breakdown of Definition df-fz
Step | Hyp | Ref
| Expression |
1 | | cfz 9965 |
. 2
class
... |
2 | | vm |
. . 3
setvar 𝑚 |
3 | | vn |
. . 3
setvar 𝑛 |
4 | | cz 9212 |
. . 3
class
ℤ |
5 | 2 | cv 1347 |
. . . . . 6
class 𝑚 |
6 | | vk |
. . . . . . 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 | 7, 10, 8 | wbr 3989 |
. . . . 5
wff 𝑘 ≤ 𝑛 |
12 | 9, 11 | wa 103 |
. . . 4
wff (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛) |
13 | 12, 6, 4 | crab 2452 |
. . 3
class {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)} |
14 | 2, 3, 4, 4, 13 | cmpo 5855 |
. 2
class (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)}) |
15 | 1, 14 | wceq 1348 |
1
wff ... =
(𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)}) |