Theorem ackvalsuc0val

Description: The Ackermann function at a successor (of the first argument). This is the second equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024)

	Ref	Expression
Assertion	ackvalsuc0val	⊢ ( 𝑀 ∈ ℕ0 → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 0 ) = ( ( Ack ‘ 𝑀 ) ‘ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		ackvalsuc1	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 0 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 0 + 1 ) ) ‘ 1 ) )
3	1 2	mpan2	⊢ ( 𝑀 ∈ ℕ0 → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 0 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 0 + 1 ) ) ‘ 1 ) )
4		0p1e1	⊢ ( 0 + 1 ) = 1
5	4	a1i	⊢ ( 𝑀 ∈ ℕ0 → ( 0 + 1 ) = 1 )
6	5	fveq2d	⊢ ( 𝑀 ∈ ℕ0 → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 0 + 1 ) ) = ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 1 ) )
7		ackfnnn0	⊢ ( 𝑀 ∈ ℕ0 → ( Ack ‘ 𝑀 ) Fn ℕ0 )
8		fnfun	⊢ ( ( Ack ‘ 𝑀 ) Fn ℕ0 → Fun ( Ack ‘ 𝑀 ) )
9		funrel	⊢ ( Fun ( Ack ‘ 𝑀 ) → Rel ( Ack ‘ 𝑀 ) )
10	7 8 9	3syl	⊢ ( 𝑀 ∈ ℕ0 → Rel ( Ack ‘ 𝑀 ) )
11		fvex	⊢ ( Ack ‘ 𝑀 ) ∈ V
12		itcoval1	⊢ ( ( Rel ( Ack ‘ 𝑀 ) ∧ ( Ack ‘ 𝑀 ) ∈ V ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 1 ) = ( Ack ‘ 𝑀 ) )
13	10 11 12	sylancl	⊢ ( 𝑀 ∈ ℕ0 → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 1 ) = ( Ack ‘ 𝑀 ) )
14	6 13	eqtrd	⊢ ( 𝑀 ∈ ℕ0 → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 0 + 1 ) ) = ( Ack ‘ 𝑀 ) )
15	14	fveq1d	⊢ ( 𝑀 ∈ ℕ0 → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 0 + 1 ) ) ‘ 1 ) = ( ( Ack ‘ 𝑀 ) ‘ 1 ) )
16	3 15	eqtrd	⊢ ( 𝑀 ∈ ℕ0 → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 0 ) = ( ( Ack ‘ 𝑀 ) ‘ 1 ) )