Metamath Proof Explorer

Theorem ackvalsuc1mpt

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

Ref Expression
Assertion ackvalsuc1mpt 
|- ( M e. NN0 -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) )

Proof

Step Hyp Ref Expression
1 df-ack 
 |-  Ack = seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) )
2 1 fveq1i 
 |-  ( Ack ` ( M + 1 ) ) = ( seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ) ` ( M + 1 ) )
3 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
4 id 
 |-  ( M e. NN0 -> M e. NN0 )
5 eqid 
 |-  ( M + 1 ) = ( M + 1 )
6 1 eqcomi 
 |-  seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ) = Ack
7 6 fveq1i 
 |-  ( seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ) ` M ) = ( Ack ` M )
8 7 a1i 
 |-  ( M e. NN0 -> ( seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ) ` M ) = ( Ack ` M ) )
9 eqidd 
 |-  ( M e. NN0 -> ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) = ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) )
10 nn0p1gt0 
 |-  ( M e. NN0 -> 0 < ( M + 1 ) )
11 10 gt0ne0d 
 |-  ( M e. NN0 -> ( M + 1 ) =/= 0 )
12 11 adantr 
 |-  ( ( M e. NN0 /\ i = ( M + 1 ) ) -> ( M + 1 ) =/= 0 )
13 neeq1 
 |-  ( i = ( M + 1 ) -> ( i =/= 0 <-> ( M + 1 ) =/= 0 ) )
14 13 adantl 
 |-  ( ( M e. NN0 /\ i = ( M + 1 ) ) -> ( i =/= 0 <-> ( M + 1 ) =/= 0 ) )
15 12 14 mpbird 
 |-  ( ( M e. NN0 /\ i = ( M + 1 ) ) -> i =/= 0 )
16 15 neneqd 
 |-  ( ( M e. NN0 /\ i = ( M + 1 ) ) -> -. i = 0 )
17 16 iffalsed 
 |-  ( ( M e. NN0 /\ i = ( M + 1 ) ) -> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) = i )
18 simpr 
 |-  ( ( M e. NN0 /\ i = ( M + 1 ) ) -> i = ( M + 1 ) )
19 17 18 eqtrd 
 |-  ( ( M e. NN0 /\ i = ( M + 1 ) ) -> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) = ( M + 1 ) )
20 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
21 9 19 20 20 fvmptd 
 |-  ( M e. NN0 -> ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` ( M + 1 ) ) = ( M + 1 ) )
22 3 4 5 8 21 seqp1d 
 |-  ( M e. NN0 -> ( seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ) ` ( M + 1 ) ) = ( ( Ack ` M ) ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) ( M + 1 ) ) )
23 eqidd 
 |-  ( M e. NN0 -> ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) = ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) )
24 fveq2 
 |-  ( f = ( Ack ` M ) -> ( IterComp ` f ) = ( IterComp ` ( Ack ` M ) ) )
25 24 fveq1d 
 |-  ( f = ( Ack ` M ) -> ( ( IterComp ` f ) ` ( n + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) )
26 25 fveq1d 
 |-  ( f = ( Ack ` M ) -> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) )
27 26 mpteq2dv 
 |-  ( f = ( Ack ` M ) -> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) )
28 27 ad2antrl 
 |-  ( ( M e. NN0 /\ ( f = ( Ack ` M ) /\ j = ( M + 1 ) ) ) -> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) )
29 fvexd 
 |-  ( M e. NN0 -> ( Ack ` M ) e. _V )
30 ovexd 
 |-  ( M e. NN0 -> ( M + 1 ) e. _V )
31 nn0ex 
 |-  NN0 e. _V
32 31 mptex 
 |-  ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) e. _V
33 32 a1i 
 |-  ( M e. NN0 -> ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) e. _V )
34 23 28 29 30 33 ovmpod 
 |-  ( M e. NN0 -> ( ( Ack ` M ) ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) )
35 22 34 eqtrd 
 |-  ( M e. NN0 -> ( seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ) ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) )
36 2 35 syl5eq 
 |-  ( M e. NN0 -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) )