Metamath Proof Explorer

Theorem ackval0

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

Ref Expression
Assertion ackval0 ⊢ Ack ⁡ 0 = n ∈ ℕ 0 ⟼ n + 1

Proof

Step Hyp Ref Expression
1 df-ack ⊢ Ack = seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i
2 1 fveq1i ⊢ Ack ⁡ 0 = seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ 0
3 0z ⊢ 0 ∈ ℤ
4 seq1 ⊢ 0 ∈ ℤ → seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ 0 = i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ 0
5 3 4 ax-mp ⊢ seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ 0 = i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ 0
6 0nn0 ⊢ 0 ∈ ℕ 0
7 iftrue ⊢ i = 0 → if i = 0 n ∈ ℕ 0 ⟼ n + 1 i = n ∈ ℕ 0 ⟼ n + 1
8 eqid ⊢ i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i = i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i
9 nn0ex ⊢ ℕ 0 ∈ V
10 9 mptex ⊢ n ∈ ℕ 0 ⟼ n + 1 ∈ V
11 7 8 10 fvmpt ⊢ 0 ∈ ℕ 0 → i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ 0 = n ∈ ℕ 0 ⟼ n + 1
12 6 11 ax-mp ⊢ i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ 0 = n ∈ ℕ 0 ⟼ n + 1
13 2 5 12 3eqtri ⊢ Ack ⁡ 0 = n ∈ ℕ 0 ⟼ n + 1