Metamath Proof Explorer


Definition df-itco

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)

Ref Expression
Assertion df-itco IterComp = f V seq 0 g V , j V f g i 0 if i = 0 I dom f f

Detailed syntax breakdown

Step Hyp Ref Expression
0 citco class IterComp
1 vf setvar f
2 cvv class V
3 cc0 class 0
4 vg setvar g
5 vj setvar j
6 1 cv setvar f
7 4 cv setvar g
8 6 7 ccom class f g
9 4 5 2 2 8 cmpo class g V , j V f g
10 vi setvar i
11 cn0 class 0
12 10 cv setvar i
13 12 3 wceq wff i = 0
14 cid class I
15 6 cdm class dom f
16 14 15 cres class I dom f
17 13 16 6 cif class if i = 0 I dom f f
18 10 11 17 cmpt class i 0 if i = 0 I dom f f
19 9 18 3 cseq class seq 0 g V , j V f g i 0 if i = 0 I dom f f
20 1 2 19 cmpt class f V seq 0 g V , j V f g i 0 if i = 0 I dom f f
21 0 20 wceq wff IterComp = f V seq 0 g V , j V f g i 0 if i = 0 I dom f f