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 φ A V
itcovalendof.f φ F : A A
itcovalendof.n φ N 0
Assertion itcovalendof Could not format assertion : No typesetting found for |- ( ph -> ( ( IterComp ` F ) ` N ) : A --> A ) with typecode |-

Proof

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