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 e. _V |-> seq 0 ( ( g e. _V , j e. _V |-> ( f o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 citco 
 |-  IterComp
1 vf 
 |-  f
2 cvv 
 |-  _V
3 cc0 
 |-  0
4 vg 
 |-  g
5 vj 
 |-  j
6 1 cv 
 |-  f
7 4 cv 
 |-  g
8 6 7 ccom 
 |-  ( f o. g )
9 4 5 2 2 8 cmpo 
 |-  ( g e. _V , j e. _V |-> ( f o. g ) )
10 vi 
 |-  i
11 cn0 
 |-  NN0
12 10 cv 
 |-  i
13 12 3 wceq 
 |-  i = 0
14 cid 
 |-  _I
15 6 cdm 
 |-  dom f
16 14 15 cres 
 |-  ( _I |` dom f )
17 13 16 6 cif 
 |-  if ( i = 0 , ( _I |` dom f ) , f )
18 10 11 17 cmpt 
 |-  ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) )
19 9 18 3 cseq 
 |-  seq 0 ( ( g e. _V , j e. _V |-> ( f o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) ) )
20 1 2 19 cmpt 
 |-  ( f e. _V |-> seq 0 ( ( g e. _V , j e. _V |-> ( f o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) ) ) )
21 0 20 wceq 
 |-  IterComp = ( f e. _V |-> seq 0 ( ( g e. _V , j e. _V |-> ( f o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) ) ) )