Definition df-itco 45678

Description: Define a function (recursively) that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.)

Assertion

Ref	Expression
df-itco	⊢ IterComp = (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))))

Distinct variable group:   𝑓,𝑔,𝑖,𝑗

Detailed syntax breakdown of Definition df-itco

Step	Hyp	Ref	Expression
1		citco 45676	. 2 class IterComp
2		vf	. . 3 setvar 𝑓
3		cvv 3408	. . 3 class V
4		vg	. . . . 5 setvar 𝑔
5		vj	. . . . 5 setvar 𝑗
6	2	cv 1542	. . . . . 6 class 𝑓
7	4	cv 1542	. . . . . 6 class 𝑔
8	6, 7	ccom 5555	. . . . 5 class (𝑓 ∘ 𝑔)
9	4, 5, 3, 3, 8	cmpo 7215	. . . 4 class (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔))
10		vi	. . . . 5 setvar 𝑖
11		cn0 12090	. . . . 5 class ℕ0
12	10	cv 1542	. . . . . . 7 class 𝑖
13		cc0 10729	. . . . . . 7 class 0
14	12, 13	wceq 1543	. . . . . 6 wff 𝑖 = 0
15		cid 5454	. . . . . . 7 class I
16	6	cdm 5551	. . . . . . 7 class dom 𝑓
17	15, 16	cres 5553	. . . . . 6 class ( I ↾ dom 𝑓)
18	14, 17, 6	cif 4439	. . . . 5 class if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓)
19	10, 11, 18	cmpt 5135	. . . 4 class (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))
20	9, 19, 13	cseq 13574	. . 3 class seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓)))
21	2, 3, 20	cmpt 5135	. 2 class (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))))
22	1, 21	wceq 1543	1 wff IterComp = (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))))

This definition is referenced by:  itcoval  45680