Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 ackvalsuc1 
 |-  ( ( M e. NN0 /\ 0 e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) )
3 1 2 mpan2 
 |-  ( M e. NN0 -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) )
4 0p1e1 
 |-  ( 0 + 1 ) = 1
5 4 a1i 
 |-  ( M e. NN0 -> ( 0 + 1 ) = 1 )
6 5 fveq2d 
 |-  ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` 1 ) )
7 ackfnnn0 
 |-  ( M e. NN0 -> ( Ack ` M ) Fn NN0 )
8 fnfun 
 |-  ( ( Ack ` M ) Fn NN0 -> Fun ( Ack ` M ) )
9 funrel 
 |-  ( Fun ( Ack ` M ) -> Rel ( Ack ` M ) )
10 7 8 9 3syl 
 |-  ( M e. NN0 -> Rel ( Ack ` M ) )
11 fvex 
 |-  ( Ack ` M ) e. _V
12 itcoval1 
 |-  ( ( Rel ( Ack ` M ) /\ ( Ack ` M ) e. _V ) -> ( ( IterComp ` ( Ack ` M ) ) ` 1 ) = ( Ack ` M ) )
13 10 11 12 sylancl 
 |-  ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` 1 ) = ( Ack ` M ) )
14 6 13 eqtrd 
 |-  ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) = ( Ack ` M ) )
15 14 fveq1d 
 |-  ( M e. NN0 -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) = ( ( Ack ` M ) ` 1 ) )
16 3 15 eqtrd 
 |-  ( M e. NN0 -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( Ack ` M ) ` 1 ) )