Theorem ackvalsuc1

Description: The Ackermann function at a successor of the first argument and an arbitrary second argument. (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 4-May-2024)

	Ref	Expression
Assertion	ackvalsuc1	Could not format assertion : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` N ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ackvalsuc1mpt	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 |-
2	1	adantr	Could not format ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( ( M e. NN0 /\ N e. NN0 ) -> ( Ack ` ( M + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode |-
3		fvoveq1	Could not format ( n = N -> ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) : No typesetting found for |- ( n = N -> ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ) with typecode |-
4	3	fveq1d	Could not format ( n = N -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) : No typesetting found for |- ( n = N -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) with typecode |-
5	4	adantl	Could not format ( ( ( M e. NN0 /\ N e. NN0 ) /\ n = N ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) : No typesetting found for |- ( ( ( M e. NN0 /\ N e. NN0 ) /\ n = N ) -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( n + 1 ) ) ` 1 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( N + 1 ) ) ` 1 ) ) with typecode |-
6		simpr	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
7		fvexd	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 |-
8	2 5 6 7	fvmptd	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 |-