Theorem itcoval

Description: The value of the function that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by AV, 2-May-2024)

	Ref	Expression
Assertion	itcoval	Could not format assertion : No typesetting found for |- ( F e. V -> ( IterComp ` F ) = seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-itco	Could not format IterComp = ( f e. _V |-> seq 0 ( ( g e. _V , j e. _V |-> ( f o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) ) ) ) : No typesetting found for |- IterComp = ( f e. _V |-> seq 0 ( ( g e. _V , j e. _V |-> ( f o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom f ) , f ) ) ) ) with typecode |-
2		eqidd	$$⊢f=F\to 0=0$$
3		coeq1	$$⊢f=F\to f\circ g=F\circ g$$
4	3	mpoeq3dv	$$⊢f=F\to \left(g\in \mathrm{V},j\in \mathrm{V}⟼f\circ g\right)=\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right)$$
5		dmeq	$$⊢f=F\to \mathrm{dom}f=\mathrm{dom}F$$
6	5	reseq2d	$$⊢f=F\to {\mathrm{I}\upharpoonright }_{\mathrm{dom}f}={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
7		id	$$⊢f=F\to f=F$$
8	6 7	ifeq12d	$$⊢f=F\to if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}f},f\right)=if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)$$
9	8	mpteq2dv	$$⊢f=F\to \left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}f},f\right)\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)\right)$$
10	2 4 9	seqeq123d	$$⊢f=F\to seq0\left(\left(g\in \mathrm{V},j\in \mathrm{V}⟼f\circ g\right),\left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}f},f\right)\right)\right)=seq0\left(\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right),\left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)\right)\right)$$
11		elex	$$⊢F\in V\to F\in \mathrm{V}$$
12		seqex	$$⊢seq0\left(\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right),\left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)\right)\right)\in \mathrm{V}$$
13	12	a1i	$$⊢F\in V\to seq0\left(\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right),\left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)\right)\right)\in \mathrm{V}$$
14	1 10 11 13	fvmptd3	Could not format ( F e. V -> ( IterComp ` F ) = seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ) : No typesetting found for |- ( F e. V -> ( IterComp ` F ) = seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ) with typecode |-