Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12511 |
. . 3
β’ (π β β0
β (π + 1) β
β0) |
2 | | ackvalsuc1 47355 |
. . 3
β’ ((π β β0
β§ (π + 1) β
β0) β ((Ackβ(π + 1))β(π + 1)) = (((IterCompβ(Ackβπ))β((π + 1) + 1))β1)) |
3 | 1, 2 | sylan2 593 |
. 2
β’ ((π β β0
β§ π β
β0) β ((Ackβ(π + 1))β(π + 1)) = (((IterCompβ(Ackβπ))β((π + 1) + 1))β1)) |
4 | | fvexd 6906 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β (Ackβπ) β V) |
5 | 1 | adantl 482 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β (π + 1) β
β0) |
6 | | eqidd 2733 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))β(π + 1)) = ((IterCompβ(Ackβπ))β(π + 1))) |
7 | | itcovalsucov 47344 |
. . . . 5
β’
(((Ackβπ)
β V β§ (π + 1)
β β0 β§ ((IterCompβ(Ackβπ))β(π + 1)) = ((IterCompβ(Ackβπ))β(π + 1))) β
((IterCompβ(Ackβπ))β((π + 1) + 1)) = ((Ackβπ) β ((IterCompβ(Ackβπ))β(π + 1)))) |
8 | 4, 5, 6, 7 | syl3anc 1371 |
. . . 4
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))β((π + 1) + 1)) = ((Ackβπ) β ((IterCompβ(Ackβπ))β(π + 1)))) |
9 | 8 | fveq1d 6893 |
. . 3
β’ ((π β β0
β§ π β
β0) β (((IterCompβ(Ackβπ))β((π + 1) + 1))β1) = (((Ackβπ) β
((IterCompβ(Ackβπ))β(π + 1)))β1)) |
10 | | ackfnnn0 47361 |
. . . . . . 7
β’ (π β β0
β (Ackβπ) Fn
β0) |
11 | 10 | adantr 481 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β (Ackβπ) Fn β0) |
12 | | nn0ex 12477 |
. . . . . . . . 9
β’
β0 β V |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ ((π β β0
β§ π β
β0) β β0 β V) |
14 | | ackendofnn0 47360 |
. . . . . . . . 9
β’ (π β β0
β (Ackβπ):β0βΆβ0) |
15 | 14 | adantr 481 |
. . . . . . . 8
β’ ((π β β0
β§ π β
β0) β (Ackβπ):β0βΆβ0) |
16 | | simpr 485 |
. . . . . . . 8
β’ ((π β β0
β§ π β
β0) β π β
β0) |
17 | 13, 15, 16 | itcovalendof 47345 |
. . . . . . 7
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))βπ):β0βΆβ0) |
18 | 17 | ffnd 6718 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))βπ) Fn β0) |
19 | 17 | frnd 6725 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β ran ((IterCompβ(Ackβπ))βπ) β
β0) |
20 | | fnco 6667 |
. . . . . 6
β’
(((Ackβπ) Fn
β0 β§ ((IterCompβ(Ackβπ))βπ) Fn β0 β§ ran
((IterCompβ(Ackβπ))βπ) β β0) β
((Ackβπ) β
((IterCompβ(Ackβπ))βπ)) Fn β0) |
21 | 11, 18, 19, 20 | syl3anc 1371 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β ((Ackβπ) β ((IterCompβ(Ackβπ))βπ)) Fn β0) |
22 | | eqidd 2733 |
. . . . . . 7
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))βπ) = ((IterCompβ(Ackβπ))βπ)) |
23 | | itcovalsucov 47344 |
. . . . . . 7
β’
(((Ackβπ)
β V β§ π β
β0 β§ ((IterCompβ(Ackβπ))βπ) = ((IterCompβ(Ackβπ))βπ)) β ((IterCompβ(Ackβπ))β(π + 1)) = ((Ackβπ) β ((IterCompβ(Ackβπ))βπ))) |
24 | 4, 16, 22, 23 | syl3anc 1371 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))β(π + 1)) = ((Ackβπ) β ((IterCompβ(Ackβπ))βπ))) |
25 | 24 | fneq1d 6642 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β (((IterCompβ(Ackβπ))β(π + 1)) Fn β0 β
((Ackβπ) β
((IterCompβ(Ackβπ))βπ)) Fn β0)) |
26 | 21, 25 | mpbird 256 |
. . . 4
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))β(π + 1)) Fn
β0) |
27 | | 1nn0 12487 |
. . . 4
β’ 1 β
β0 |
28 | | fvco2 6988 |
. . . 4
β’
((((IterCompβ(Ackβπ))β(π + 1)) Fn β0 β§ 1 β
β0) β (((Ackβπ) β ((IterCompβ(Ackβπ))β(π + 1)))β1) = ((Ackβπ)β(((IterCompβ(Ackβπ))β(π + 1))β1))) |
29 | 26, 27, 28 | sylancl 586 |
. . 3
β’ ((π β β0
β§ π β
β0) β (((Ackβπ) β ((IterCompβ(Ackβπ))β(π + 1)))β1) = ((Ackβπ)β(((IterCompβ(Ackβπ))β(π + 1))β1))) |
30 | 9, 29 | eqtrd 2772 |
. 2
β’ ((π β β0
β§ π β
β0) β (((IterCompβ(Ackβπ))β((π + 1) + 1))β1) = ((Ackβπ)β(((IterCompβ(Ackβπ))β(π + 1))β1))) |
31 | | ackvalsuc1 47355 |
. . . 4
β’ ((π β β0
β§ π β
β0) β ((Ackβ(π + 1))βπ) = (((IterCompβ(Ackβπ))β(π + 1))β1)) |
32 | 31 | eqcomd 2738 |
. . 3
β’ ((π β β0
β§ π β
β0) β (((IterCompβ(Ackβπ))β(π + 1))β1) = ((Ackβ(π + 1))βπ)) |
33 | 32 | fveq2d 6895 |
. 2
β’ ((π β β0
β§ π β
β0) β ((Ackβπ)β(((IterCompβ(Ackβπ))β(π + 1))β1)) = ((Ackβπ)β((Ackβ(π + 1))βπ))) |
34 | 3, 30, 33 | 3eqtrd 2776 |
1
β’ ((π β β0
β§ π β
β0) β ((Ackβ(π + 1))β(π + 1)) = ((Ackβπ)β((Ackβ(π + 1))βπ))) |