This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )