Theorem ackvalsuc1

Description: The Ackermann function at a successor of the first argument and an arbitrary second argument. (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 4-May-2024)

	Ref	Expression
Assertion	ackvalsuc1	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 𝑁 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		ackvalsuc1mpt	⊢ ( 𝑀 ∈ ℕ0 → ( Ack ‘ ( 𝑀 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
2	1	adantr	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( Ack ‘ ( 𝑀 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
3		fvoveq1	⊢ ( 𝑛 = 𝑁 → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) )
4	3	fveq1d	⊢ ( 𝑛 = 𝑁 → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) )
5	4	adantl	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 = 𝑁 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) )
6		simpr	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
7		fvexd	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) ∈ V )
8	2 5 6 7	fvmptd	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 𝑁 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) )