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\in {\mathbb{N}}_0\to \mathrm{Ack}\left(M\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢x=0\to \mathrm{Ack}\left(x\right)=\mathrm{Ack}\left(0\right)$$
2	1	feq1d	$$⊢x=0\to \left(\mathrm{Ack}\left(x\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\leftrightarrow \mathrm{Ack}\left(0\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)$$
3		fveq2	$$⊢x=y\to \mathrm{Ack}\left(x\right)=\mathrm{Ack}\left(y\right)$$
4	3	feq1d	$$⊢x=y\to \left(\mathrm{Ack}\left(x\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\leftrightarrow \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)$$
5		fveq2	$$⊢x=y+1\to \mathrm{Ack}\left(x\right)=\mathrm{Ack}\left(y+1\right)$$
6	5	feq1d	$$⊢x=y+1\to \left(\mathrm{Ack}\left(x\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\leftrightarrow \mathrm{Ack}\left(y+1\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)$$
7		fveq2	$$⊢x=M\to \mathrm{Ack}\left(x\right)=\mathrm{Ack}\left(M\right)$$
8	7	feq1d	$$⊢x=M\to \left(\mathrm{Ack}\left(x\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\leftrightarrow \mathrm{Ack}\left(M\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)$$
9		ackval0	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)$$
10		peano2nn0	$$⊢n\in {\mathbb{N}}_0\to n+1\in {\mathbb{N}}_0$$
11	9 10	fmpti	$$⊢\mathrm{Ack}\left(0\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
12		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
13	12	a1i	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
14		simplr	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
15	10	adantl	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to n+1\in {\mathbb{N}}_0$$
16	13 14 15	itcovalendof	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
17		1nn0	$$⊢1\in {\mathbb{N}}_0$$
18		ffvelcdm	$$⊢\left(\mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right)\left(1\right)\in {\mathbb{N}}_0$$
19	16 17 18	sylancl	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right)\left(1\right)\in {\mathbb{N}}_0$$
20		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right)\left(1\right)\right)=\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right)\left(1\right)\right)$$
21	19 20	fmptd	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right)\left(1\right)\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
22		ackvalsuc1mpt	$$⊢y\in {\mathbb{N}}_0\to \mathrm{Ack}\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right)\left(1\right)\right)$$
23	22	adantr	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\to \mathrm{Ack}\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right)\left(1\right)\right)$$
24	23	feq1d	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\to \left(\mathrm{Ack}\left(y+1\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\leftrightarrow \left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(y\right)\right)\left(n+1\right)\left(1\right)\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)$$
25	21 24	mpbird	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\to \mathrm{Ack}\left(y+1\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
26	25	ex	$$⊢y\in {\mathbb{N}}_0\to \left(\mathrm{Ack}\left(y\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\to \mathrm{Ack}\left(y+1\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)$$
27	2 4 6 8 11 26	nn0ind	$$⊢M\in {\mathbb{N}}_0\to \mathrm{Ack}\left(M\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$