Step | Hyp | Ref
| Expression |
1 | | cack 47334 |
. 2
class
Ack |
2 | | vf |
. . . 4
setvar π |
3 | | vj |
. . . 4
setvar π |
4 | | cvv 3474 |
. . . 4
class
V |
5 | | vn |
. . . . 5
setvar π |
6 | | cn0 12471 |
. . . . 5
class
β0 |
7 | | c1 11110 |
. . . . . 6
class
1 |
8 | 5 | cv 1540 |
. . . . . . . 8
class π |
9 | | caddc 11112 |
. . . . . . . 8
class
+ |
10 | 8, 7, 9 | co 7408 |
. . . . . . 7
class (π + 1) |
11 | 2 | cv 1540 |
. . . . . . . 8
class π |
12 | | citco 47333 |
. . . . . . . 8
class
IterComp |
13 | 11, 12 | cfv 6543 |
. . . . . . 7
class
(IterCompβπ) |
14 | 10, 13 | cfv 6543 |
. . . . . 6
class
((IterCompβπ)β(π + 1)) |
15 | 7, 14 | cfv 6543 |
. . . . 5
class
(((IterCompβπ)β(π + 1))β1) |
16 | 5, 6, 15 | cmpt 5231 |
. . . 4
class (π β β0
β¦ (((IterCompβπ)β(π + 1))β1)) |
17 | 2, 3, 4, 4, 16 | cmpo 7410 |
. . 3
class (π β V, π β V β¦ (π β β0 β¦
(((IterCompβπ)β(π + 1))β1))) |
18 | | vi |
. . . 4
setvar π |
19 | 18 | cv 1540 |
. . . . . 6
class π |
20 | | cc0 11109 |
. . . . . 6
class
0 |
21 | 19, 20 | wceq 1541 |
. . . . 5
wff π = 0 |
22 | 5, 6, 10 | cmpt 5231 |
. . . . 5
class (π β β0
β¦ (π +
1)) |
23 | 21, 22, 19 | cif 4528 |
. . . 4
class if(π = 0, (π β β0 β¦ (π + 1)), π) |
24 | 18, 6, 23 | cmpt 5231 |
. . 3
class (π β β0
β¦ if(π = 0, (π β β0
β¦ (π + 1)), π)) |
25 | 17, 24, 20 | cseq 13965 |
. 2
class
seq0((π β V,
π β V β¦ (π β β0
β¦ (((IterCompβπ)β(π + 1))β1))), (π β β0 β¦ if(π = 0, (π β β0 β¦ (π + 1)), π))) |
26 | 1, 25 | wceq 1541 |
1
wff Ack =
seq0((π β V, π β V β¦ (π β β0
β¦ (((IterCompβπ)β(π + 1))β1))), (π β β0 β¦ if(π = 0, (π β β0 β¦ (π + 1)), π))) |