Theorem itcoval0

Description: A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024)

	Ref	Expression
Assertion	itcoval0	Could not format assertion : No typesetting found for |- ( F e. V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom F ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		itcoval	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 |-
2	1	fveq1d	Could not format ( F e. V -> ( ( IterComp ` F ) ` 0 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 0 ) ) : No typesetting found for |- ( F e. V -> ( ( IterComp ` F ) ` 0 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 0 ) ) with typecode |-
3		0z	$$⊢0\in \mathbb{Z}$$
4		eqidd	$$⊢F\in V\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)$$
5		iftrue	$$⊢i=0\to if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
6	5	adantl	$$⊢\left(F\in V\wedge i=0\right)\to if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
7		0nn0	$$⊢0\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢F\in V\to 0\in {\mathbb{N}}_0$$
9		dmexg	$$⊢F\in V\to \mathrm{dom}F\in \mathrm{V}$$
10	9	resiexd	$$⊢F\in V\to {\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\in \mathrm{V}$$
11	4 6 8 10	fvmptd	$$⊢F\in V\to \left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)\right)\left(0\right)={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
12	3 11	seq1i	$$⊢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)\left(0\right)={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
13	2 12	eqtrd	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 |-