Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12512 |
. . 3
β’ (π β β0
β (π + 1) β
β0) |
2 | | ackvalsuc1 47365 |
. . 3
β’ ((π β β0
β§ (π + 1) β
β0) β ((Ackβ(π + 1))β(π + 1)) = (((IterCompβ(Ackβπ))β((π + 1) + 1))β1)) |
3 | 1, 2 | sylan2 594 |
. 2
β’ ((π β β0
β§ π β
β0) β ((Ackβ(π + 1))β(π + 1)) = (((IterCompβ(Ackβπ))β((π + 1) + 1))β1)) |
4 | | fvexd 6907 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β (Ackβπ) β V) |
5 | 1 | adantl 483 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β (π + 1) β
β0) |
6 | | eqidd 2734 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))β(π + 1)) = ((IterCompβ(Ackβπ))β(π + 1))) |
7 | | itcovalsucov 47354 |
. . . . 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 1372 |
. . . 4
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))β((π + 1) + 1)) = ((Ackβπ) β ((IterCompβ(Ackβπ))β(π + 1)))) |
9 | 8 | fveq1d 6894 |
. . 3
β’ ((π β β0
β§ π β
β0) β (((IterCompβ(Ackβπ))β((π + 1) + 1))β1) = (((Ackβπ) β
((IterCompβ(Ackβπ))β(π + 1)))β1)) |
10 | | ackfnnn0 47371 |
. . . . . . 7
β’ (π β β0
β (Ackβπ) Fn
β0) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β (Ackβπ) Fn β0) |
12 | | nn0ex 12478 |
. . . . . . . . 9
β’
β0 β V |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ ((π β β0
β§ π β
β0) β β0 β V) |
14 | | ackendofnn0 47370 |
. . . . . . . . 9
β’ (π β β0
β (Ackβπ):β0βΆβ0) |
15 | 14 | adantr 482 |
. . . . . . . 8
β’ ((π β β0
β§ π β
β0) β (Ackβπ):β0βΆβ0) |
16 | | simpr 486 |
. . . . . . . 8
β’ ((π β β0
β§ π β
β0) β π β
β0) |
17 | 13, 15, 16 | itcovalendof 47355 |
. . . . . . 7
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))βπ):β0βΆβ0) |
18 | 17 | ffnd 6719 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))βπ) Fn β0) |
19 | 17 | frnd 6726 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β ran ((IterCompβ(Ackβπ))βπ) β
β0) |
20 | | fnco 6668 |
. . . . . 6
β’
(((Ackβπ) Fn
β0 β§ ((IterCompβ(Ackβπ))βπ) Fn β0 β§ ran
((IterCompβ(Ackβπ))βπ) β β0) β
((Ackβπ) β
((IterCompβ(Ackβπ))βπ)) Fn β0) |
21 | 11, 18, 19, 20 | syl3anc 1372 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β ((Ackβπ) β ((IterCompβ(Ackβπ))βπ)) Fn β0) |
22 | | eqidd 2734 |
. . . . . . 7
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))βπ) = ((IterCompβ(Ackβπ))βπ)) |
23 | | itcovalsucov 47354 |
. . . . . . 7
β’
(((Ackβπ)
β V β§ π β
β0 β§ ((IterCompβ(Ackβπ))βπ) = ((IterCompβ(Ackβπ))βπ)) β ((IterCompβ(Ackβπ))β(π + 1)) = ((Ackβπ) β ((IterCompβ(Ackβπ))βπ))) |
24 | 4, 16, 22, 23 | syl3anc 1372 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))β(π + 1)) = ((Ackβπ) β ((IterCompβ(Ackβπ))βπ))) |
25 | 24 | fneq1d 6643 |
. . . . 5
β’ ((π β β0
β§ π β
β0) β (((IterCompβ(Ackβπ))β(π + 1)) Fn β0 β
((Ackβπ) β
((IterCompβ(Ackβπ))βπ)) Fn β0)) |
26 | 21, 25 | mpbird 257 |
. . . 4
β’ ((π β β0
β§ π β
β0) β ((IterCompβ(Ackβπ))β(π + 1)) Fn
β0) |
27 | | 1nn0 12488 |
. . . 4
β’ 1 β
β0 |
28 | | fvco2 6989 |
. . . 4
β’
((((IterCompβ(Ackβπ))β(π + 1)) Fn β0 β§ 1 β
β0) β (((Ackβπ) β ((IterCompβ(Ackβπ))β(π + 1)))β1) = ((Ackβπ)β(((IterCompβ(Ackβπ))β(π + 1))β1))) |
29 | 26, 27, 28 | sylancl 587 |
. . 3
β’ ((π β β0
β§ π β
β0) β (((Ackβπ) β ((IterCompβ(Ackβπ))β(π + 1)))β1) = ((Ackβπ)β(((IterCompβ(Ackβπ))β(π + 1))β1))) |
30 | 9, 29 | eqtrd 2773 |
. 2
β’ ((π β β0
β§ π β
β0) β (((IterCompβ(Ackβπ))β((π + 1) + 1))β1) = ((Ackβπ)β(((IterCompβ(Ackβπ))β(π + 1))β1))) |
31 | | ackvalsuc1 47365 |
. . . 4
β’ ((π β β0
β§ π β
β0) β ((Ackβ(π + 1))βπ) = (((IterCompβ(Ackβπ))β(π + 1))β1)) |
32 | 31 | eqcomd 2739 |
. . 3
β’ ((π β β0
β§ π β
β0) β (((IterCompβ(Ackβπ))β(π + 1))β1) = ((Ackβ(π + 1))βπ)) |
33 | 32 | fveq2d 6896 |
. 2
β’ ((π β β0
β§ π β
β0) β ((Ackβπ)β(((IterCompβ(Ackβπ))β(π + 1))β1)) = ((Ackβπ)β((Ackβ(π + 1))βπ))) |
34 | 3, 30, 33 | 3eqtrd 2777 |
1
β’ ((π β β0
β§ π β
β0) β ((Ackβ(π + 1))β(π + 1)) = ((Ackβπ)β((Ackβ(π + 1))βπ))) |