Definition df-ack 47394

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

Assertion

Ref	Expression
df-ack	⊢ Ack = seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))

Distinct variable group:   𝑓,𝑖,𝑗,𝑛

Detailed syntax breakdown of Definition df-ack

Step	Hyp	Ref	Expression
1		cack 47392	. 2 class Ack
2		vf	. . . 4 setvar 𝑓
3		vj	. . . 4 setvar 𝑗
4		cvv 3475	. . . 4 class V
5		vn	. . . . 5 setvar 𝑛
6		cn0 12472	. . . . 5 class ℕ0
7		c1 11111	. . . . . 6 class 1
8	5	cv 1541	. . . . . . . 8 class 𝑛
9		caddc 11113	. . . . . . . 8 class +
10	8, 7, 9	co 7409	. . . . . . 7 class (𝑛 + 1)
11	2	cv 1541	. . . . . . . 8 class 𝑓
12		citco 47391	. . . . . . . 8 class IterComp
13	11, 12	cfv 6544	. . . . . . 7 class (IterComp‘𝑓)
14	10, 13	cfv 6544	. . . . . 6 class ((IterComp‘𝑓)‘(𝑛 + 1))
15	7, 14	cfv 6544	. . . . 5 class (((IterComp‘𝑓)‘(𝑛 + 1))‘1)
16	5, 6, 15	cmpt 5232	. . . 4 class (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))
17	2, 3, 4, 4, 16	cmpo 7411	. . 3 class (𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1)))
18		vi	. . . 4 setvar 𝑖
19	18	cv 1541	. . . . . 6 class 𝑖
20		cc0 11110	. . . . . 6 class 0
21	19, 20	wceq 1542	. . . . 5 wff 𝑖 = 0
22	5, 6, 10	cmpt 5232	. . . . 5 class (𝑛 ∈ ℕ0 ↦ (𝑛 + 1))
23	21, 22, 19	cif 4529	. . . 4 class if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)
24	18, 6, 23	cmpt 5232	. . 3 class (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))
25	17, 24, 20	cseq 13966	. 2 class seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))
26	1, 25	wceq 1542	1 wff Ack = seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))

This definition is referenced by:  ackvalsuc1mpt  47412  ackval0  47414