Metamath Proof Explorer

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 
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` N ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) )

Proof

Step Hyp Ref Expression
1 ackvalsuc1mpt 
 |-  ( M e. NN0 -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) )
2 1 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) )
3 fvoveq1 
 |-  ( n = N -> ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) )
4 3 fveq1d 
 |-  ( n = N -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) )
5 4 adantl 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ n = N ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) )
6 simpr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> N e. NN0 )
7 fvexd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) e. _V )
8 2 5 6 7 fvmptd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` N ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) )