Theorem ackval0val

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

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

Proof

Step	Hyp	Ref	Expression
1		ackval0	⊢ ( Ack ‘ 0 ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 + 1 ) )
2	1	a1i	⊢ ( 𝑀 ∈ ℕ0 → ( Ack ‘ 0 ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 + 1 ) ) )
3		oveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 + 1 ) = ( 𝑀 + 1 ) )
4	3	adantl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑚 = 𝑀 ) → ( 𝑚 + 1 ) = ( 𝑀 + 1 ) )
5		id	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℕ0 )
6		peano2nn0	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
7	2 4 5 6	fvmptd	⊢ ( 𝑀 ∈ ℕ0 → ( ( Ack ‘ 0 ) ‘ 𝑀 ) = ( 𝑀 + 1 ) )