Detailed syntax breakdown of Definition df-ef
Step | Hyp | Ref
| Expression |
1 | | ce 14631 |
. 2
class
exp |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cc 9813 |
. . 3
class
ℂ |
4 | | cn0 11169 |
. . . 4
class
ℕ0 |
5 | 2 | cv 1474 |
. . . . . 6
class 𝑥 |
6 | | vk |
. . . . . . 7
setvar 𝑘 |
7 | 6 | cv 1474 |
. . . . . 6
class 𝑘 |
8 | | cexp 12722 |
. . . . . 6
class
↑ |
9 | 5, 7, 8 | co 6549 |
. . . . 5
class (𝑥↑𝑘) |
10 | | cfa 12922 |
. . . . . 6
class
! |
11 | 7, 10 | cfv 5804 |
. . . . 5
class
(!‘𝑘) |
12 | | cdiv 10563 |
. . . . 5
class
/ |
13 | 9, 11, 12 | co 6549 |
. . . 4
class ((𝑥↑𝑘) / (!‘𝑘)) |
14 | 4, 13, 6 | csu 14264 |
. . 3
class
Σ𝑘 ∈
ℕ0 ((𝑥↑𝑘) / (!‘𝑘)) |
15 | 2, 3, 14 | cmpt 4643 |
. 2
class (𝑥 ∈ ℂ ↦
Σ𝑘 ∈
ℕ0 ((𝑥↑𝑘) / (!‘𝑘))) |
16 | 1, 15 | wceq 1475 |
1
wff exp =
(𝑥 ∈ ℂ ↦
Σ𝑘 ∈
ℕ0 ((𝑥↑𝑘) / (!‘𝑘))) |