Theorem ackfnnn0

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

	Ref	Expression
Assertion	ackfnnn0	$$⊢M\in {\mathbb{N}}_0\to \mathrm{Ack}\left(M\right)Fn{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		ackendofnn0	$$⊢M\in {\mathbb{N}}_0\to \mathrm{Ack}\left(M\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
2		ffn	$$⊢\mathrm{Ack}\left(M\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\to \mathrm{Ack}\left(M\right)Fn{\mathbb{N}}_0$$
3	1 2	syl	$$⊢M\in {\mathbb{N}}_0\to \mathrm{Ack}\left(M\right)Fn{\mathbb{N}}_0$$