This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackval0012

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

Ref Expression
Assertion ackval0012 
|- <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >.

Proof

Step Hyp Ref Expression
1 ackval0 
 |-  ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) )
2 oveq1 
 |-  ( n = 0 -> ( n + 1 ) = ( 0 + 1 ) )
3 0p1e1 
 |-  ( 0 + 1 ) = 1
4 2 3 eqtrdi 
 |-  ( n = 0 -> ( n + 1 ) = 1 )
5 0nn0 
 |-  0 e. NN0
6 5 a1i 
 |-  ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 0 e. NN0 )
7 1nn0 
 |-  1 e. NN0
8 7 a1i 
 |-  ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 1 e. NN0 )
9 1 4 6 8 fvmptd3 
 |-  ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 0 ) = 1 )
10 oveq1 
 |-  ( n = 1 -> ( n + 1 ) = ( 1 + 1 ) )
11 1p1e2 
 |-  ( 1 + 1 ) = 2
12 10 11 eqtrdi 
 |-  ( n = 1 -> ( n + 1 ) = 2 )
13 2nn0 
 |-  2 e. NN0
14 13 a1i 
 |-  ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 2 e. NN0 )
15 1 12 8 14 fvmptd3 
 |-  ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 1 ) = 2 )
16 oveq1 
 |-  ( n = 2 -> ( n + 1 ) = ( 2 + 1 ) )
17 2p1e3 
 |-  ( 2 + 1 ) = 3
18 16 17 eqtrdi 
 |-  ( n = 2 -> ( n + 1 ) = 3 )
19 3nn0 
 |-  3 e. NN0
20 19 a1i 
 |-  ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 3 e. NN0 )
21 1 18 14 20 fvmptd3 
 |-  ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 2 ) = 3 )
22 9 15 21 oteq123d 
 |-  ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. )
23 1 22 ax-mp 
 |-  <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >.