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 )