Theorem ackval0

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

	Ref	Expression
Assertion	ackval0	⊢ ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ack	⊢ Ack = seq 0 ( ( 𝑓 ∈ V , 𝑗 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) )
2	1	fveq1i	⊢ ( Ack ‘ 0 ) = ( seq 0 ( ( 𝑓 ∈ V , 𝑗 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) ) ‘ 0 )
3		0z	⊢ 0 ∈ ℤ
4		seq1	⊢ ( 0 ∈ ℤ → ( seq 0 ( ( 𝑓 ∈ V , 𝑗 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) ) ‘ 0 ) = ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) ‘ 0 ) )
5	3 4	ax-mp	⊢ ( seq 0 ( ( 𝑓 ∈ V , 𝑗 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) ) ‘ 0 ) = ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) ‘ 0 )
6		0nn0	⊢ 0 ∈ ℕ0
7		iftrue	⊢ ( 𝑖 = 0 → if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) )
8		eqid	⊢ ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) )
9		nn0ex	⊢ ℕ0 ∈ V
10	9	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) ∈ V
11	7 8 10	fvmpt	⊢ ( 0 ∈ ℕ0 → ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) )
12	6 11	ax-mp	⊢ ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) )
13	2 5 12	3eqtri	⊢ ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) )