Definition df-itco

Description: Define a function (recursively) that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 2-May-2024)

	Ref	Expression
Assertion	df-itco	Could not format assertion : 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 |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citco	Could not format IterComp : No typesetting found for class IterComp with typecode class
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		cc0	$$class0$$
4		vg	$$setvarg$$
5		vj	$$setvarj$$
6	1	cv	$$setvarf$$
7	4	cv	$$setvarg$$
8	6 7	ccom	$$class\left(f\circ g\right)$$
9	4 5 2 2 8	cmpo	$$class\left(g\in \mathrm{V},j\in \mathrm{V}⟼f\circ g\right)$$
10		vi	$$setvari$$
11		cn0	$$class{\mathbb{N}}_0$$
12	10	cv	$$setvari$$
13	12 3	wceq	$$wffi=0$$
14		cid	$$class\mathrm{I}$$
15	6	cdm	$$class\mathrm{dom}f$$
16	14 15	cres	$$class\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}f}\right)$$
17	13 16 6	cif	$$classif\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}f},f\right)$$
18	10 11 17	cmpt	$$class\left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}f},f\right)\right)$$
19	9 18 3	cseq	$$classseq0\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)$$
20	1 2 19	cmpt	$$class\left(f\in \mathrm{V}⟼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)\right)$$
21	0 20	wceq	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 wff 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 wff