Metamath Proof Explorer

Theorem ackvalsucsucval

Description: The Ackermann function at the successors. This is the third equation of Péter's definition of the Ackermann function. (Contributed by AV, 8-May-2024)

Ref Expression
Assertion ackvalsucsucval 
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( Ack ` M ) ` ( ( Ack ` ( M + 1 ) ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
2 ackvalsuc1 
 |-  ( ( M e. NN0 /\ ( N + 1 ) e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) )
3 1 2 sylan2 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) )
4 fvexd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) e. _V )
5 1 adantl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N + 1 ) e. NN0 )
6 eqidd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) )
7 itcovalsucov 
 |-  ( ( ( Ack ` M ) e. _V /\ ( N + 1 ) e. NN0 /\ ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) = ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) )
8 4 5 6 7 syl3anc 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) = ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) )
9 8 fveq1d 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) = ( ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ` 1 ) )
10 ackfnnn0 
 |-  ( M e. NN0 -> ( Ack ` M ) Fn NN0 )
11 10 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) Fn NN0 )
12 nn0ex 
 |-  NN0 e. _V
13 12 a1i 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> NN0 e. _V )
14 ackendofnn0 
 |-  ( M e. NN0 -> ( Ack ` M ) : NN0 --> NN0 )
15 14 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) : NN0 --> NN0 )
16 simpr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> N e. NN0 )
17 13 15 16 itcovalendof 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) : NN0 --> NN0 )
18 17 ffnd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) Fn NN0 )
19 17 frnd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ran ( ( IterComp ` ( Ack ` M ) ) ` N ) C_ NN0 )
20 fnco 
 |-  ( ( ( Ack ` M ) Fn NN0 /\ ( ( IterComp ` ( Ack ` M ) ) ` N ) Fn NN0 /\ ran ( ( IterComp ` ( Ack ` M ) ) ` N ) C_ NN0 ) -> ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) Fn NN0 )
21 11 18 19 20 syl3anc 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) Fn NN0 )
22 eqidd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) = ( ( IterComp ` ( Ack ` M ) ) ` N ) )
23 itcovalsucov 
 |-  ( ( ( Ack ` M ) e. _V /\ N e. NN0 /\ ( ( IterComp ` ( Ack ` M ) ) ` N ) = ( ( IterComp ` ( Ack ` M ) ) ` N ) ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) = ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) )
24 4 16 22 23 syl3anc 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) = ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) )
25 24 fneq1d 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) Fn NN0 <-> ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) Fn NN0 ) )
26 21 25 mpbird 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) Fn NN0 )
27 1nn0 
 |-  1 e. NN0
28 fvco2 
 |-  ( ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) Fn NN0 /\ 1 e. NN0 ) -> ( ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ` 1 ) = ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) )
29 26 27 28 sylancl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ` 1 ) = ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) )
30 9 29 eqtrd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) = ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) )
31 ackvalsuc1 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` N ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) )
32 31 eqcomd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) = ( ( Ack ` ( M + 1 ) ) ` N ) )
33 32 fveq2d 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) = ( ( Ack ` M ) ` ( ( Ack ` ( M + 1 ) ) ` N ) ) )
34 3 30 33 3eqtrd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( Ack ` M ) ` ( ( Ack ` ( M + 1 ) ) ` N ) ) )