Metamath Proof Explorer


Theorem ackendofnn0

Description: The Ackermann function at any nonnegative integer is an endofunction on the nonnegative integers. (Contributed by AV, 8-May-2024)

Ref Expression
Assertion ackendofnn0 M 0 Ack M : 0 0

Proof

Step Hyp Ref Expression
1 fveq2 x = 0 Ack x = Ack 0
2 1 feq1d x = 0 Ack x : 0 0 Ack 0 : 0 0
3 fveq2 x = y Ack x = Ack y
4 3 feq1d x = y Ack x : 0 0 Ack y : 0 0
5 fveq2 x = y + 1 Ack x = Ack y + 1
6 5 feq1d x = y + 1 Ack x : 0 0 Ack y + 1 : 0 0
7 fveq2 x = M Ack x = Ack M
8 7 feq1d x = M Ack x : 0 0 Ack M : 0 0
9 ackval0 Ack 0 = n 0 n + 1
10 peano2nn0 n 0 n + 1 0
11 9 10 fmpti Ack 0 : 0 0
12 nn0ex 0 V
13 12 a1i y 0 Ack y : 0 0 n 0 0 V
14 simplr y 0 Ack y : 0 0 n 0 Ack y : 0 0
15 10 adantl y 0 Ack y : 0 0 n 0 n + 1 0
16 13 14 15 itcovalendof y 0 Ack y : 0 0 n 0 IterComp Ack y n + 1 : 0 0
17 1nn0 1 0
18 ffvelcdm IterComp Ack y n + 1 : 0 0 1 0 IterComp Ack y n + 1 1 0
19 16 17 18 sylancl y 0 Ack y : 0 0 n 0 IterComp Ack y n + 1 1 0
20 eqid n 0 IterComp Ack y n + 1 1 = n 0 IterComp Ack y n + 1 1
21 19 20 fmptd y 0 Ack y : 0 0 n 0 IterComp Ack y n + 1 1 : 0 0
22 ackvalsuc1mpt y 0 Ack y + 1 = n 0 IterComp Ack y n + 1 1
23 22 adantr y 0 Ack y : 0 0 Ack y + 1 = n 0 IterComp Ack y n + 1 1
24 23 feq1d y 0 Ack y : 0 0 Ack y + 1 : 0 0 n 0 IterComp Ack y n + 1 1 : 0 0
25 21 24 mpbird y 0 Ack y : 0 0 Ack y + 1 : 0 0
26 25 ex y 0 Ack y : 0 0 Ack y + 1 : 0 0
27 2 4 6 8 11 26 nn0ind M 0 Ack M : 0 0