Detailed syntax breakdown of Definition df-naryf
Step | Hyp | Ref
| Expression |
1 | | cnaryf 45390 |
. 2
class
-aryF |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | vx |
. . 3
setvar 𝑥 |
4 | | cn0 11919 |
. . 3
class
ℕ0 |
5 | | cvv 3407 |
. . 3
class
V |
6 | 3 | cv 1538 |
. . . 4
class 𝑥 |
7 | | cc0 10560 |
. . . . . 6
class
0 |
8 | 2 | cv 1538 |
. . . . . 6
class 𝑛 |
9 | | cfzo 13067 |
. . . . . 6
class
..^ |
10 | 7, 8, 9 | co 7143 |
. . . . 5
class
(0..^𝑛) |
11 | | cmap 8409 |
. . . . 5
class
↑m |
12 | 6, 10, 11 | co 7143 |
. . . 4
class (𝑥 ↑m (0..^𝑛)) |
13 | 6, 12, 11 | co 7143 |
. . 3
class (𝑥 ↑m (𝑥 ↑m (0..^𝑛))) |
14 | 2, 3, 4, 5, 13 | cmpo 7145 |
. 2
class (𝑛 ∈ ℕ0,
𝑥 ∈ V ↦ (𝑥 ↑m (𝑥 ↑m (0..^𝑛)))) |
15 | 1, 14 | wceq 1539 |
1
wff -aryF =
(𝑛 ∈
ℕ0, 𝑥
∈ V ↦ (𝑥
↑m (𝑥
↑m (0..^𝑛)))) |