Definition df-ack 45424

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 45422	. 2 class Ack
2		vf	. . . 4 setvar 𝑓
3		vj	. . . 4 setvar 𝑗
4		cvv 3407	. . . 4 class V
5		vn	. . . . 5 setvar 𝑛
6		cn0 11919	. . . . 5 class ℕ0
7		c1 10561	. . . . . 6 class 1
8	5	cv 1538	. . . . . . . 8 class 𝑛
9		caddc 10563	. . . . . . . 8 class +
10	8, 7, 9	co 7143	. . . . . . 7 class (𝑛 + 1)
11	2	cv 1538	. . . . . . . 8 class 𝑓
12		citco 45421	. . . . . . . 8 class IterComp
13	11, 12	cfv 6328	. . . . . . 7 class (IterComp‘𝑓)
14	10, 13	cfv 6328	. . . . . 6 class ((IterComp‘𝑓)‘(𝑛 + 1))
15	7, 14	cfv 6328	. . . . 5 class (((IterComp‘𝑓)‘(𝑛 + 1))‘1)
16	5, 6, 15	cmpt 5105	. . . 4 class (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))
17	2, 3, 4, 4, 16	cmpo 7145	. . 3 class (𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1)))
18		vi	. . . 4 setvar 𝑖
19	18	cv 1538	. . . . . 6 class 𝑖
20		cc0 10560	. . . . . 6 class 0
21	19, 20	wceq 1539	. . . . 5 wff 𝑖 = 0
22	5, 6, 10	cmpt 5105	. . . . 5 class (𝑛 ∈ ℕ0 ↦ (𝑛 + 1))
23	21, 22, 19	cif 4413	. . . 4 class if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)
24	18, 6, 23	cmpt 5105	. . 3 class (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))
25	17, 24, 20	cseq 13403	. 2 class seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))
26	1, 25	wceq 1539	1 wff Ack = seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))

This definition is referenced by:  ackvalsuc1mpt  45442  ackval0  45444