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	Could not format assertion : No typesetting found for |- ( M e. NN0 -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-ack	Could not format 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 ) ) ) : No typesetting found for |- 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 ) ) ) with typecode |-
2	1	fveq1i	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
3		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
4		id	$$⊢M\in {\mathbb{N}}_0\to M\in {\mathbb{N}}_0$$
5		eqid	$$⊢M+1=M+1$$
6	1	eqcomi	Could not format 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 : No typesetting found for |- 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 with typecode |-
7	6	fveq1i	Could not format ( 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 ) : No typesetting found for |- ( 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 ) with typecode |-
8	7	a1i	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
9		eqidd	$$⊢M\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼if\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)\right)$$
10		nn0p1gt0	$$⊢M\in {\mathbb{N}}_0\to 0<M+1$$
11	10	gt0ne0d	$$⊢M\in {\mathbb{N}}_0\to M+1\ne 0$$
12	11	adantr	$$⊢\left(M\in {\mathbb{N}}_0\wedge i=M+1\right)\to M+1\ne 0$$
13		neeq1	$$⊢i=M+1\to \left(i\ne 0\leftrightarrow M+1\ne 0\right)$$
14	13	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge i=M+1\right)\to \left(i\ne 0\leftrightarrow M+1\ne 0\right)$$
15	12 14	mpbird	$$⊢\left(M\in {\mathbb{N}}_0\wedge i=M+1\right)\to i\ne 0$$
16	15	neneqd	$$⊢\left(M\in {\mathbb{N}}_0\wedge i=M+1\right)\to \neg i=0$$
17	16	iffalsed	$$⊢\left(M\in {\mathbb{N}}_0\wedge i=M+1\right)\to if\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)=i$$
18		simpr	$$⊢\left(M\in {\mathbb{N}}_0\wedge i=M+1\right)\to i=M+1$$
19	17 18	eqtrd	$$⊢\left(M\in {\mathbb{N}}_0\wedge i=M+1\right)\to if\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)=M+1$$
20		peano2nn0	$$⊢M\in {\mathbb{N}}_0\to M+1\in {\mathbb{N}}_0$$
21	9 19 20 20	fvmptd	$$⊢M\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼if\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)\right)\left(M+1\right)=M+1$$
22	3 4 5 8 21	seqp1d	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
23		eqidd	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
24		fveq2	Could not format ( f = ( Ack ` M ) -> ( IterComp ` f ) = ( IterComp ` ( Ack ` M ) ) ) : No typesetting found for |- ( f = ( Ack ` M ) -> ( IterComp ` f ) = ( IterComp ` ( Ack ` M ) ) ) with typecode |-
25	24	fveq1d	Could not format ( f = ( Ack ` M ) -> ( ( IterComp ` f ) ` ( n + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ) : No typesetting found for |- ( f = ( Ack ` M ) -> ( ( IterComp ` f ) ` ( n + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ) with typecode |-
26	25	fveq1d	Could not format ( f = ( Ack ` M ) -> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) : No typesetting found for |- ( f = ( Ack ` M ) -> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) with typecode |-
27	26	mpteq2dv	Could not format ( f = ( Ack ` M ) -> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( f = ( Ack ` M ) -> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode |-
28	27	ad2antrl	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
29		fvexd	Could not format ( M e. NN0 -> ( Ack ` M ) e. _V ) : No typesetting found for |- ( M e. NN0 -> ( Ack ` M ) e. _V ) with typecode |-
30		ovexd	$$⊢M\in {\mathbb{N}}_0\to M+1\in \mathrm{V}$$
31		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
32	31	mptex	Could not format ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) e. _V : No typesetting found for |- ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) e. _V with typecode |-
33	32	a1i	Could not format ( M e. NN0 -> ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) e. _V ) : No typesetting found for |- ( M e. NN0 -> ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) e. _V ) with typecode |-
34	23 28 29 30 33	ovmpod	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
35	22 34	eqtrd	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
36	2 35	syl5eq	Could not format ( M e. NN0 -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( M e. NN0 -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode |-