Metamath Proof Explorer

Theorem itcovalendof

Description: The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024)

Ref Expression
Hypotheses itcovalendof.a 
|- ( ph -> A e. V )
itcovalendof.f 
|- ( ph -> F : A --> A )
itcovalendof.n 
|- ( ph -> N e. NN0 )
Assertion itcovalendof 
|- ( ph -> ( ( IterComp ` F ) ` N ) : A --> A )

Proof

Step Hyp Ref Expression
1 itcovalendof.a 
 |-  ( ph -> A e. V )
2 itcovalendof.f 
 |-  ( ph -> F : A --> A )
3 itcovalendof.n 
 |-  ( ph -> N e. NN0 )
4 fveq2 
 |-  ( x = 0 -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` 0 ) )
5 4 feq1d 
 |-  ( x = 0 -> ( ( ( IterComp ` F ) ` x ) : A --> A <-> ( ( IterComp ` F ) ` 0 ) : A --> A ) )
6 fveq2 
 |-  ( x = y -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` y ) )
7 6 feq1d 
 |-  ( x = y -> ( ( ( IterComp ` F ) ` x ) : A --> A <-> ( ( IterComp ` F ) ` y ) : A --> A ) )
8 fveq2 
 |-  ( x = ( y + 1 ) -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` ( y + 1 ) ) )
9 8 feq1d 
 |-  ( x = ( y + 1 ) -> ( ( ( IterComp ` F ) ` x ) : A --> A <-> ( ( IterComp ` F ) ` ( y + 1 ) ) : A --> A ) )
10 fveq2 
 |-  ( x = N -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` N ) )
11 10 feq1d 
 |-  ( x = N -> ( ( ( IterComp ` F ) ` x ) : A --> A <-> ( ( IterComp ` F ) ` N ) : A --> A ) )
12 f1oi 
 |-  ( _I |` A ) : A -1-1-onto-> A
13 f1of 
 |-  ( ( _I |` A ) : A -1-1-onto-> A -> ( _I |` A ) : A --> A )
14 12 13 mp1i 
 |-  ( ph -> ( _I |` A ) : A --> A )
15 2 fdmd 
 |-  ( ph -> dom F = A )
16 15 reseq2d 
 |-  ( ph -> ( _I |` dom F ) = ( _I |` A ) )
17 16 feq1d 
 |-  ( ph -> ( ( _I |` dom F ) : A --> A <-> ( _I |` A ) : A --> A ) )
18 14 17 mpbird 
 |-  ( ph -> ( _I |` dom F ) : A --> A )
19 2 1 fexd 
 |-  ( ph -> F e. _V )
20 itcoval0 
 |-  ( F e. _V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom F ) )
21 19 20 syl 
 |-  ( ph -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom F ) )
22 21 feq1d 
 |-  ( ph -> ( ( ( IterComp ` F ) ` 0 ) : A --> A <-> ( _I |` dom F ) : A --> A ) )
23 18 22 mpbird 
 |-  ( ph -> ( ( IterComp ` F ) ` 0 ) : A --> A )
24 2 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> F : A --> A )
25 simpr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> ( ( IterComp ` F ) ` y ) : A --> A )
26 24 25 fcod 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> ( F o. ( ( IterComp ` F ) ` y ) ) : A --> A )
27 19 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> F e. _V )
28 simplr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> y e. NN0 )
29 eqidd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> ( ( IterComp ` F ) ` y ) = ( ( IterComp ` F ) ` y ) )
30 itcovalsucov 
 |-  ( ( F e. _V /\ y e. NN0 /\ ( ( IterComp ` F ) ` y ) = ( ( IterComp ` F ) ` y ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( ( IterComp ` F ) ` y ) ) )
31 27 28 29 30 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( ( IterComp ` F ) ` y ) ) )
32 31 feq1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> ( ( ( IterComp ` F ) ` ( y + 1 ) ) : A --> A <-> ( F o. ( ( IterComp ` F ) ` y ) ) : A --> A ) )
33 26 32 mpbird 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) : A --> A ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) : A --> A )
34 5 7 9 11 23 33 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( ( IterComp ` F ) ` N ) : A --> A )
35 3 34 mpdan 
 |-  ( ph -> ( ( IterComp ` F ) ` N ) : A --> A )