Metamath Proof Explorer

Theorem ackendofnn0

Description: The Ackermann function at any nonnegative integer is an endofunction on the nonnegative integers. (Contributed by AV, 8-May-2024)

Ref Expression
Assertion ackendofnn0 Could not format assertion : No typesetting found for |- ( M e. NN0 -> ( Ack ` M ) : NN0 --> NN0 ) with typecode |-

Proof

Step Hyp Ref Expression
1 fveq2 Could not format ( x = 0 -> ( Ack ` x ) = ( Ack ` 0 ) ) : No typesetting found for |- ( x = 0 -> ( Ack ` x ) = ( Ack ` 0 ) ) with typecode |-
2 1 feq1d Could not format ( x = 0 -> ( ( Ack ` x ) : NN0 --> NN0 <-> ( Ack ` 0 ) : NN0 --> NN0 ) ) : No typesetting found for |- ( x = 0 -> ( ( Ack ` x ) : NN0 --> NN0 <-> ( Ack ` 0 ) : NN0 --> NN0 ) ) with typecode |-
3 fveq2 Could not format ( x = y -> ( Ack ` x ) = ( Ack ` y ) ) : No typesetting found for |- ( x = y -> ( Ack ` x ) = ( Ack ` y ) ) with typecode |-
4 3 feq1d Could not format ( x = y -> ( ( Ack ` x ) : NN0 --> NN0 <-> ( Ack ` y ) : NN0 --> NN0 ) ) : No typesetting found for |- ( x = y -> ( ( Ack ` x ) : NN0 --> NN0 <-> ( Ack ` y ) : NN0 --> NN0 ) ) with typecode |-
5 fveq2 Could not format ( x = ( y + 1 ) -> ( Ack ` x ) = ( Ack ` ( y + 1 ) ) ) : No typesetting found for |- ( x = ( y + 1 ) -> ( Ack ` x ) = ( Ack ` ( y + 1 ) ) ) with typecode |-
6 5 feq1d Could not format ( x = ( y + 1 ) -> ( ( Ack ` x ) : NN0 --> NN0 <-> ( Ack ` ( y + 1 ) ) : NN0 --> NN0 ) ) : No typesetting found for |- ( x = ( y + 1 ) -> ( ( Ack ` x ) : NN0 --> NN0 <-> ( Ack ` ( y + 1 ) ) : NN0 --> NN0 ) ) with typecode |-
7 fveq2 Could not format ( x = M -> ( Ack ` x ) = ( Ack ` M ) ) : No typesetting found for |- ( x = M -> ( Ack ` x ) = ( Ack ` M ) ) with typecode |-
8 7 feq1d Could not format ( x = M -> ( ( Ack ` x ) : NN0 --> NN0 <-> ( Ack ` M ) : NN0 --> NN0 ) ) : No typesetting found for |- ( x = M -> ( ( Ack ` x ) : NN0 --> NN0 <-> ( Ack ` M ) : NN0 --> NN0 ) ) with typecode |-
9 ackval0 Could not format ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) : No typesetting found for |- ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) with typecode |-
10 peano2nn0 ⊢ n ∈ ℕ 0 → n + 1 ∈ ℕ 0
11 9 10 fmpti Could not format ( Ack ` 0 ) : NN0 --> NN0 : No typesetting found for |- ( Ack ` 0 ) : NN0 --> NN0 with typecode |-
12 nn0ex ⊢ ℕ 0 ∈ V
13 12 a1i Could not format ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> NN0 e. _V ) : No typesetting found for |- ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> NN0 e. _V ) with typecode |-
14 simplr Could not format ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> ( Ack ` y ) : NN0 --> NN0 ) : No typesetting found for |- ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> ( Ack ` y ) : NN0 --> NN0 ) with typecode |-
15 10 adantl Could not format ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> ( n + 1 ) e. NN0 ) : No typesetting found for |- ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> ( n + 1 ) e. NN0 ) with typecode |-
16 13 14 15 itcovalendof Could not format ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) : NN0 --> NN0 ) : No typesetting found for |- ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) : NN0 --> NN0 ) with typecode |-
17 1nn0 ⊢ 1 ∈ ℕ 0
18 ffvelrn Could not format ( ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) : NN0 --> NN0 /\ 1 e. NN0 ) -> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) e. NN0 ) : No typesetting found for |- ( ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) : NN0 --> NN0 /\ 1 e. NN0 ) -> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) e. NN0 ) with typecode |-
19 16 17 18 sylancl Could not format ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) e. NN0 ) : No typesetting found for |- ( ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) /\ n e. NN0 ) -> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) e. NN0 ) with typecode |-
20 eqid Could not format ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) : No typesetting found for |- ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) with typecode |-
21 19 20 fmptd Could not format ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) -> ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) : NN0 --> NN0 ) : No typesetting found for |- ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) -> ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) : NN0 --> NN0 ) with typecode |-
22 ackvalsuc1mpt Could not format ( y e. NN0 -> ( Ack ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( y e. NN0 -> ( Ack ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode |-
23 22 adantr Could not format ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) -> ( Ack ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) -> ( Ack ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode |-
24 23 feq1d Could not format ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) -> ( ( Ack ` ( y + 1 ) ) : NN0 --> NN0 <-> ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) : NN0 --> NN0 ) ) : No typesetting found for |- ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) -> ( ( Ack ` ( y + 1 ) ) : NN0 --> NN0 <-> ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` y ) ) ` ( n + 1 ) ) ` 1 ) ) : NN0 --> NN0 ) ) with typecode |-
25 21 24 mpbird Could not format ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) -> ( Ack ` ( y + 1 ) ) : NN0 --> NN0 ) : No typesetting found for |- ( ( y e. NN0 /\ ( Ack ` y ) : NN0 --> NN0 ) -> ( Ack ` ( y + 1 ) ) : NN0 --> NN0 ) with typecode |-
26 25 ex Could not format ( y e. NN0 -> ( ( Ack ` y ) : NN0 --> NN0 -> ( Ack ` ( y + 1 ) ) : NN0 --> NN0 ) ) : No typesetting found for |- ( y e. NN0 -> ( ( Ack ` y ) : NN0 --> NN0 -> ( Ack ` ( y + 1 ) ) : NN0 --> NN0 ) ) with typecode |-
27 2 4 6 8 11 26 nn0ind Could not format ( M e. NN0 -> ( Ack ` M ) : NN0 --> NN0 ) : No typesetting found for |- ( M e. NN0 -> ( Ack ` M ) : NN0 --> NN0 ) with typecode |-