Theorem ackval0

Description: The Ackermann function at 0. (Contributed by AV, 2-May-2024)

	Ref	Expression
Assertion	ackval0	Could not format assertion : No typesetting found for |- ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 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 ` 0 ) = ( 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 ) ) ) ` 0 ) : No typesetting found for |- ( Ack ` 0 ) = ( 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 ) ) ) ` 0 ) with typecode |-
3		0z	$$⊢0\in \mathbb{Z}$$
4		seq1	Could not format ( 0 e. ZZ -> ( 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 ) ) ) ` 0 ) = ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` 0 ) ) : No typesetting found for |- ( 0 e. ZZ -> ( 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 ) ) ) ` 0 ) = ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` 0 ) ) with typecode |-
5	3 4	ax-mp	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 ) ) ) ` 0 ) = ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` 0 ) : 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 ) ) ) ` 0 ) = ( ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) ` 0 ) with typecode |-
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7		iftrue	$$⊢i=0\to if\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)$$
8		eqid	$$⊢\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)$$
9		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
10	9	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼n+1\right)\in \mathrm{V}$$
11	7 8 10	fvmpt	$$⊢0\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(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)$$
12	6 11	ax-mp	$$⊢\left(i\in {\mathbb{N}}_0⟼if\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+1\right)$$
13	2 5 12	3eqtri	Could not format ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) : No typesetting found for |- ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) with typecode |-