Metamath Proof Explorer

Definition df-ack

Description: Define the Ackermann function (recursively). (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 2-May-2024)

Ref Expression
Assertion 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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cack class Ack
1 cc0 class 0
2 vf setvar f
3 cvv class V
4 vj setvar j
5 vn setvar n
6 cn0 class ℕ 0
7 citco class IterComp
8 2 cv setvar f
9 8 7 cfv class IterComp ⁡ f
10 5 cv setvar n
11 caddc class +
12 c1 class 1
13 10 12 11 co class n + 1
14 13 9 cfv class IterComp ⁡ f ⁡ n + 1
15 12 14 cfv class IterComp ⁡ f ⁡ n + 1 ⁡ 1
16 5 6 15 cmpt class n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1
17 2 4 3 3 16 cmpo class f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1
18 vi setvar i
19 18 cv setvar i
20 19 1 wceq wff i = 0
21 5 6 13 cmpt class n ∈ ℕ 0 ⟼ n + 1
22 20 21 19 cif class if i = 0 n ∈ ℕ 0 ⟼ n + 1 i
23 18 6 22 cmpt class i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i
24 17 23 1 cseq class seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i
25 0 24 wceq wff Ack = seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i