Definition df-ack 47919

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 47917	. 2 class Ack
2		vf	. . . 4 setvar 𝑓
3		vj	. . . 4 setvar 𝑗
4		cvv 3461	. . . 4 class V
5		vn	. . . . 5 setvar 𝑛
6		cn0 12505	. . . . 5 class ℕ0
7		c1 11141	. . . . . 6 class 1
8	5	cv 1532	. . . . . . . 8 class 𝑛
9		caddc 11143	. . . . . . . 8 class +
10	8, 7, 9	co 7419	. . . . . . 7 class (𝑛 + 1)
11	2	cv 1532	. . . . . . . 8 class 𝑓
12		citco 47916	. . . . . . . 8 class IterComp
13	11, 12	cfv 6549	. . . . . . 7 class (IterComp‘𝑓)
14	10, 13	cfv 6549	. . . . . 6 class ((IterComp‘𝑓)‘(𝑛 + 1))
15	7, 14	cfv 6549	. . . . 5 class (((IterComp‘𝑓)‘(𝑛 + 1))‘1)
16	5, 6, 15	cmpt 5232	. . . 4 class (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))
17	2, 3, 4, 4, 16	cmpo 7421	. . 3 class (𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1)))
18		vi	. . . 4 setvar 𝑖
19	18	cv 1532	. . . . . 6 class 𝑖
20		cc0 11140	. . . . . 6 class 0
21	19, 20	wceq 1533	. . . . 5 wff 𝑖 = 0
22	5, 6, 10	cmpt 5232	. . . . 5 class (𝑛 ∈ ℕ0 ↦ (𝑛 + 1))
23	21, 22, 19	cif 4530	. . . 4 class if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)
24	18, 6, 23	cmpt 5232	. . 3 class (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))
25	17, 24, 20	cseq 14002	. 2 class seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))
26	1, 25	wceq 1533	1 wff Ack = seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))

This definition is referenced by:  ackvalsuc1mpt  47937  ackval0  47939