Metamath Proof Explorer

Theorem ackval0

Description: The Ackermann function at 0. (Contributed by AV, 2-May-2024)

Ref Expression
Assertion ackval0 
|- ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 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 ` 0 ) = ( 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 ) ) ) ` 0 )
3 0z 
 |-  0 e. ZZ
4 seq1 
 |-  ( 0 e. ZZ -> ( 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 ) ) ) ` 0 ) = ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` 0 ) )
5 3 4 ax-mp 
 |-  ( 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 ) ) ) ` 0 ) = ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` 0 )
6 0nn0 
 |-  0 e. NN0
7 iftrue 
 |-  ( i = 0 -> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) = ( n e. NN0 |-> ( n + 1 ) ) )
8 eqid 
 |-  ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) = ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) )
9 nn0ex 
 |-  NN0 e. _V
10 9 mptex 
 |-  ( n e. NN0 |-> ( n + 1 ) ) e. _V
11 7 8 10 fvmpt 
 |-  ( 0 e. NN0 -> ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) )
12 6 11 ax-mp 
 |-  ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` 0 ) = ( n e. NN0 |-> ( n + 1 ) )
13 2 5 12 3eqtri 
 |-  ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) )