Theorem itcovalendof

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

	Ref	Expression
Hypotheses	itcovalendof.a	$$⊢\phi \to A\in V$$
	itcovalendof.f	$$⊢\phi \to F:A⟶A$$
	itcovalendof.n	$$⊢\phi \to N\in {\mathbb{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	$$⊢\phi \to A\in V$$
2		itcovalendof.f	$$⊢\phi \to F:A⟶A$$
3		itcovalendof.n	$$⊢\phi \to N\in {\mathbb{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	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A$$
13		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A\to \left({\mathrm{I}\upharpoonright }_A\right):A⟶A$$
14	12 13	mp1i	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_A\right):A⟶A$$
15	2	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
16	15	reseq2d	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\mathrm{dom}F}={\mathrm{I}\upharpoonright }_A$$
17	16	feq1d	$$⊢\phi \to \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right):A⟶A\leftrightarrow \left({\mathrm{I}\upharpoonright }_A\right):A⟶A\right)$$
18	14 17	mpbird	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right):A⟶A$$
19	2 1	fexd	$$⊢\phi \to F\in \mathrm{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 |-