Theorem ackval0012

Description: The Ackermann function at (0,0), (0,1), (0,2). (Contributed by AV, 2-May-2024)

	Ref	Expression
Assertion	ackval0012	$$⊢⟨\mathrm{Ack}\left(0\right)\left(0\right),\mathrm{Ack}\left(0\right)\left(1\right),\mathrm{Ack}\left(0\right)\left(2\right)⟩=⟨1,2,3⟩$$

Proof

Step	Hyp	Ref	Expression
1		ackval0	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)$$
2		oveq1	$$⊢n=0\to n+1=0+1$$
3		0p1e1	$$⊢0+1=1$$
4	2 3	eqtrdi	$$⊢n=0\to n+1=1$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)\to 0\in {\mathbb{N}}_0$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)\to 1\in {\mathbb{N}}_0$$
9	1 4 6 8	fvmptd3	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)\to \mathrm{Ack}\left(0\right)\left(0\right)=1$$
10		oveq1	$$⊢n=1\to n+1=1+1$$
11		1p1e2	$$⊢1+1=2$$
12	10 11	eqtrdi	$$⊢n=1\to n+1=2$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14	13	a1i	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)\to 2\in {\mathbb{N}}_0$$
15	1 12 8 14	fvmptd3	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)\to \mathrm{Ack}\left(0\right)\left(1\right)=2$$
16		oveq1	$$⊢n=2\to n+1=2+1$$
17		2p1e3	$$⊢2+1=3$$
18	16 17	eqtrdi	$$⊢n=2\to n+1=3$$
19		3nn0	$$⊢3\in {\mathbb{N}}_0$$
20	19	a1i	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)\to 3\in {\mathbb{N}}_0$$
21	1 18 14 20	fvmptd3	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)\to \mathrm{Ack}\left(0\right)\left(2\right)=3$$
22	9 15 21	oteq123d	$$⊢\mathrm{Ack}\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)\to ⟨\mathrm{Ack}\left(0\right)\left(0\right),\mathrm{Ack}\left(0\right)\left(1\right),\mathrm{Ack}\left(0\right)\left(2\right)⟩=⟨1,2,3⟩$$
23	1 22	ax-mp	$$⊢⟨\mathrm{Ack}\left(0\right)\left(0\right),\mathrm{Ack}\left(0\right)\left(1\right),\mathrm{Ack}\left(0\right)\left(2\right)⟩=⟨1,2,3⟩$$