Metamath Proof Explorer


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
|- ( M e. NN0 -> ( ( Ack ` 0 ) ` M ) = ( M + 1 ) )

Proof

Step Hyp Ref Expression
1 ackval0
 |-  ( Ack ` 0 ) = ( m e. NN0 |-> ( m + 1 ) )
2 1 a1i
 |-  ( M e. NN0 -> ( Ack ` 0 ) = ( m e. NN0 |-> ( m + 1 ) ) )
3 oveq1
 |-  ( m = M -> ( m + 1 ) = ( M + 1 ) )
4 3 adantl
 |-  ( ( M e. NN0 /\ m = M ) -> ( m + 1 ) = ( M + 1 ) )
5 id
 |-  ( M e. NN0 -> M e. NN0 )
6 peano2nn0
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
7 2 4 5 6 fvmptd
 |-  ( M e. NN0 -> ( ( Ack ` 0 ) ` M ) = ( M + 1 ) )