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	$$⊢\phi \to \mathrm{IterComp}\left(F\right)\left(N\right):A⟶A$$

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	$$⊢x=0\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(0\right)$$
5	4	feq1d	$$⊢x=0\to \left(\mathrm{IterComp}\left(F\right)\left(x\right):A⟶A\leftrightarrow \mathrm{IterComp}\left(F\right)\left(0\right):A⟶A\right)$$
6		fveq2	$$⊢x=y\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(y\right)$$
7	6	feq1d	$$⊢x=y\to \left(\mathrm{IterComp}\left(F\right)\left(x\right):A⟶A\leftrightarrow \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)$$
8		fveq2	$$⊢x=y+1\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(y+1\right)$$
9	8	feq1d	$$⊢x=y+1\to \left(\mathrm{IterComp}\left(F\right)\left(x\right):A⟶A\leftrightarrow \mathrm{IterComp}\left(F\right)\left(y+1\right):A⟶A\right)$$
10		fveq2	$$⊢x=N\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(N\right)$$
11	10	feq1d	$$⊢x=N\to \left(\mathrm{IterComp}\left(F\right)\left(x\right):A⟶A\leftrightarrow \mathrm{IterComp}\left(F\right)\left(N\right):A⟶A\right)$$
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	$$⊢F\in \mathrm{V}\to \mathrm{IterComp}\left(F\right)\left(0\right)={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
21	19 20	syl	$$⊢\phi \to \mathrm{IterComp}\left(F\right)\left(0\right)={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
22	21	feq1d	$$⊢\phi \to \left(\mathrm{IterComp}\left(F\right)\left(0\right):A⟶A\leftrightarrow \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right):A⟶A\right)$$
23	18 22	mpbird	$$⊢\phi \to \mathrm{IterComp}\left(F\right)\left(0\right):A⟶A$$
24	2	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to F:A⟶A$$
25		simpr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A$$
26	24 25	fcod	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to \left(F\circ \mathrm{IterComp}\left(F\right)\left(y\right)\right):A⟶A$$
27	19	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to F\in \mathrm{V}$$
28		simplr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to y\in {\mathbb{N}}_0$$
29		eqidd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to \mathrm{IterComp}\left(F\right)\left(y\right)=\mathrm{IterComp}\left(F\right)\left(y\right)$$
30		itcovalsucov	$$⊢\left(F\in \mathrm{V}\wedge y\in {\mathbb{N}}_0\wedge \mathrm{IterComp}\left(F\right)\left(y\right)=\mathrm{IterComp}\left(F\right)\left(y\right)\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=F\circ \mathrm{IterComp}\left(F\right)\left(y\right)$$
31	27 28 29 30	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=F\circ \mathrm{IterComp}\left(F\right)\left(y\right)$$
32	31	feq1d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to \left(\mathrm{IterComp}\left(F\right)\left(y+1\right):A⟶A\leftrightarrow \left(F\circ \mathrm{IterComp}\left(F\right)\left(y\right)\right):A⟶A\right)$$
33	26 32	mpbird	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right):A⟶A\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right):A⟶A$$
34	5 7 9 11 23 33	nn0indd	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(F\right)\left(N\right):A⟶A$$
35	3 34	mpdan	$$⊢\phi \to \mathrm{IterComp}\left(F\right)\left(N\right):A⟶A$$