Theorem itcoval1

Description: A function iterated once. (Contributed by AV, 2-May-2024)

	Ref	Expression
Assertion	itcoval1	Could not format assertion : No typesetting found for |- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = 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 ) ` 1 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) ) : No typesetting found for |- ( F e. V -> ( ( IterComp ` F ) ` 1 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) ) with typecode |-
3	2	adantl	Could not format ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) ) : No typesetting found for |- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) ) with typecode |-
4		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to 0\in {\mathbb{N}}_0$$
7		1e0p1	$$⊢1=0+1$$
8	1	eqcomd	Could not format ( F e. V -> seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) = ( IterComp ` F ) ) : No typesetting found for |- ( F e. V -> seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) = ( IterComp ` F ) ) with typecode |-
9	8	fveq1d	Could not format ( F e. V -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 0 ) = ( ( IterComp ` F ) ` 0 ) ) : No typesetting found for |- ( F e. V -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 0 ) = ( ( IterComp ` F ) ` 0 ) ) with typecode |-
10		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 |-
11	9 10	eqtrd	$$⊢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}$$
12	11	adantl	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\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		eqidd	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\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)$$
14		ax-1ne0	$$⊢1\ne 0$$
15	14	neii	$$⊢\neg 1=0$$
16		eqeq1	$$⊢i=1\to \left(i=0\leftrightarrow 1=0\right)$$
17	15 16	mtbiri	$$⊢i=1\to \neg i=0$$
18	17	iffalsed	$$⊢i=1\to if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)=F$$
19	18	adantl	$$⊢\left(\left(\mathrm{Rel}F\wedge F\in V\right)\wedge i=1\right)\to if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)=F$$
20		1nn0	$$⊢1\in {\mathbb{N}}_0$$
21	20	a1i	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to 1\in {\mathbb{N}}_0$$
22		simpr	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to F\in V$$
23	13 19 21 22	fvmptd	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to \left(i\in {\mathbb{N}}_0⟼if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)\right)\left(1\right)=F$$
24	4 6 7 12 23	seqp1d	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\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(1\right)=\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right)F$$
25		eqidd	$$⊢F\in V\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)$$
26		coeq2	$$⊢g={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\to F\circ g=F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)$$
27	26	ad2antrl	$$⊢\left(F\in V\wedge \left(g={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\wedge j=F\right)\right)\to F\circ g=F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)$$
28		dmexg	$$⊢F\in V\to \mathrm{dom}F\in \mathrm{V}$$
29	28	resiexd	$$⊢F\in V\to {\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\in \mathrm{V}$$
30		elex	$$⊢F\in V\to F\in \mathrm{V}$$
31		coexg	$$⊢\left(F\in V\wedge {\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\in \mathrm{V}\right)\to F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\in \mathrm{V}$$
32	29 31	mpdan	$$⊢F\in V\to F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\in \mathrm{V}$$
33	25 27 29 30 32	ovmpod	$$⊢F\in V\to \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right)F=F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)$$
34	33	adantl	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right)F=F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)$$
35		coires1	$$⊢F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)={F\upharpoonright }_{\mathrm{dom}F}$$
36		resdm	$$⊢\mathrm{Rel}F\to {F\upharpoonright }_{\mathrm{dom}F}=F$$
37	36	adantr	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to {F\upharpoonright }_{\mathrm{dom}F}=F$$
38	35 37	syl5eq	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)=F$$
39	34 38	eqtrd	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right)F=F$$
40	24 39	eqtrd	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\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(1\right)=F$$
41	3 40	eqtrd	Could not format ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = F ) : No typesetting found for |- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = F ) with typecode |-