Metamath Proof Explorer

Theorem itcovalsucov

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

Ref Expression
Assertion itcovalsucov 
|- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( F o. G ) )

Proof

Step Hyp Ref Expression
1 itcovalsuc 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) )
2 eqidd 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( g e. _V , j e. _V |-> ( F o. g ) ) = ( g e. _V , j e. _V |-> ( F o. g ) ) )
3 coeq2 
 |-  ( g = G -> ( F o. g ) = ( F o. G ) )
4 3 ad2antrl 
 |-  ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ ( g = G /\ j = F ) ) -> ( F o. g ) = ( F o. G ) )
5 id 
 |-  ( G = ( ( IterComp ` F ) ` Y ) -> G = ( ( IterComp ` F ) ` Y ) )
6 fvex 
 |-  ( ( IterComp ` F ) ` Y ) e. _V
7 5 6 eqeltrdi 
 |-  ( G = ( ( IterComp ` F ) ` Y ) -> G e. _V )
8 7 eqcoms 
 |-  ( ( ( IterComp ` F ) ` Y ) = G -> G e. _V )
9 8 3ad2ant3 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> G e. _V )
10 elex 
 |-  ( F e. V -> F e. _V )
11 10 3ad2ant1 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> F e. _V )
12 8 anim2i 
 |-  ( ( F e. V /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F e. V /\ G e. _V ) )
13 12 3adant2 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F e. V /\ G e. _V ) )
14 coexg 
 |-  ( ( F e. V /\ G e. _V ) -> ( F o. G ) e. _V )
15 13 14 syl 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F o. G ) e. _V )
16 2 4 9 11 15 ovmpod 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. G ) )
17 1 16 eqtrd 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( F o. G ) )