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

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
2		ackvalsuc1	Could not format ( ( M e. NN0 /\ ( N + 1 ) e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) ) : No typesetting found for |- ( ( M e. NN0 /\ ( N + 1 ) e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) ) with typecode |-
3	1 2	sylan2	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) ) with typecode |-
4		fvexd	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) e. _V ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) e. _V ) with typecode |-
5	1	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N+1\in {\mathbb{N}}_0$$
6		eqidd	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) with typecode |-
7		itcovalsucov	Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
8	4 5 6 7	syl3anc	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) = ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) = ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ) with typecode |-
9	8	fveq1d	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) = ( ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ` 1 ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) = ( ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ` 1 ) ) with typecode |-
10		ackfnnn0	Could not format ( M e. NN0 -> ( Ack ` M ) Fn NN0 ) : No typesetting found for |- ( M e. NN0 -> ( Ack ` M ) Fn NN0 ) with typecode |-
11	10	adantr	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) Fn NN0 ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) Fn NN0 ) with typecode |-
12		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
13	12	a1i	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
14		ackendofnn0	Could not format ( M e. NN0 -> ( Ack ` M ) : NN0 --> NN0 ) : No typesetting found for |- ( M e. NN0 -> ( Ack ` M ) : NN0 --> NN0 ) with typecode |-
15	14	adantr	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) : NN0 --> NN0 ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` M ) : NN0 --> NN0 ) with typecode |-
16		simpr	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
17	13 15 16	itcovalendof	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) : NN0 --> NN0 ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) : NN0 --> NN0 ) with typecode |-
18	17	ffnd	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) Fn NN0 ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) Fn NN0 ) with typecode |-
19	17	frnd	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ran ( ( IterComp ` ( Ack ` M ) ) ` N ) C_ NN0 ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ran ( ( IterComp ` ( Ack ` M ) ) ` N ) C_ NN0 ) with typecode |-
20		fnco	Could not format ( ( ( 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 ) : No typesetting found for |- ( ( ( 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 ) with typecode |-
21	11 18 19 20	syl3anc	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) Fn NN0 ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) Fn NN0 ) with typecode |-
22		eqidd	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) = ( ( IterComp ` ( Ack ` M ) ) ` N ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` N ) = ( ( IterComp ` ( Ack ` M ) ) ` N ) ) with typecode |-
23		itcovalsucov	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
24	4 16 22 23	syl3anc	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) = ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) = ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) ) with typecode |-
25	24	fneq1d	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) Fn NN0 <-> ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) Fn NN0 ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) Fn NN0 <-> ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` N ) ) Fn NN0 ) ) with typecode |-
26	21 25	mpbird	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) Fn NN0 ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) Fn NN0 ) with typecode |-
27		1nn0	$$⊢1\in {\mathbb{N}}_0$$
28		fvco2	Could not format ( ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-
29	26 27 28	sylancl	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ` 1 ) = ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( Ack ` M ) o. ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) ` 1 ) = ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) ) with typecode |-
30	9 29	eqtrd	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) = ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( ( N + 1 ) + 1 ) ) ` 1 ) = ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) ) with typecode |-
31		ackvalsuc1	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` N ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` N ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) with typecode |-
32	31	eqcomd	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) = ( ( Ack ` ( M + 1 ) ) ` N ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) = ( ( Ack ` ( M + 1 ) ) ` N ) ) with typecode |-
33	32	fveq2d	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) = ( ( Ack ` M ) ` ( ( Ack ` ( M + 1 ) ) ` N ) ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` M ) ` ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) = ( ( Ack ` M ) ` ( ( Ack ` ( M + 1 ) ) ` N ) ) ) with typecode |-
34	3 30 33	3eqtrd	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( Ack ` M ) ` ( ( Ack ` ( M + 1 ) ) ` N ) ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` ( N + 1 ) ) = ( ( Ack ` M ) ` ( ( Ack ` ( M + 1 ) ) ` N ) ) ) with typecode |-