Metamath Proof Explorer

Theorem itcoval

Description: The value of the function that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by AV, 2-May-2024)

Ref Expression
Assertion itcoval 
|- ( F e. V -> ( IterComp ` F ) = seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) )
2 eqidd 
 |-  ( f = F -> 0 = 0 )
3 coeq1 
 |-  ( f = F -> ( f o. g ) = ( F o. g ) )
4 3 mpoeq3dv 
 |-  ( f = F -> ( g e. _V , j e. _V |-> ( f o. g ) ) = ( g e. _V , j e. _V |-> ( F o. g ) ) )
5 dmeq 
 |-  ( f = F -> dom f = dom F )
6 5 reseq2d 
 |-  ( f = F -> ( _I |` dom f ) = ( _I |` dom F ) )
7 id 
 |-  ( f = F -> f = F )
8 6 7 ifeq12d 
 |-  ( f = F -> if ( i = 0 , ( _I |` dom f ) , f ) = if ( i = 0 , ( _I |` dom F ) , F ) )
9 8 mpteq2dv 
 |-  ( f = F -> ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) ) = ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) )
10 2 4 9 seqeq123d 
 |-  ( f = F -> seq 0 ( ( g e. _V , j e. _V |-> ( f o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) ) ) = seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) )
11 elex 
 |-  ( F e. V -> F e. _V )
12 seqex 
 |-  seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) e. _V
13 12 a1i 
 |-  ( F e. V -> seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) e. _V )
14 1 10 11 13 fvmptd3 
 |-  ( F e. V -> ( IterComp ` F ) = seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) )