Theorem itcoval2

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

	Ref	Expression
Assertion	itcoval2	Could not format assertion : No typesetting found for |- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 2 ) = ( F o. 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 ) ` 2 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 2 ) ) : No typesetting found for |- ( F e. V -> ( ( IterComp ` F ) ` 2 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 2 ) ) with typecode |-
3	2	adantl	Could not format ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 2 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 2 ) ) : No typesetting found for |- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 2 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 2 ) ) with typecode |-
4		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to 1\in {\mathbb{N}}_0$$
7		df-2	$$⊢2=1+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 ) ) ) ` 1 ) = ( ( IterComp ` F ) ` 1 ) ) : 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 ) ) ) ` 1 ) = ( ( IterComp ` F ) ` 1 ) ) with typecode |-
10	9	adantl	Could not format ( ( Rel F /\ F e. V ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) = ( ( IterComp ` F ) ` 1 ) ) : No typesetting found for |- ( ( Rel F /\ F e. V ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) = ( ( IterComp ` F ) ` 1 ) ) with typecode |-
11		itcoval1	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 |-
12	10 11	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$$
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		2ne0	$$⊢2\ne 0$$
15		neeq1	$$⊢i=2\to \left(i\ne 0\leftrightarrow 2\ne 0\right)$$
16	14 15	mpbiri	$$⊢i=2\to i\ne 0$$
17	16	neneqd	$$⊢i=2\to \neg i=0$$
18	17	iffalsed	$$⊢i=2\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=2\right)\to if\left(i=0,{\mathrm{I}\upharpoonright }_{\mathrm{dom}F},F\right)=F$$
20		2nn0	$$⊢2\in {\mathbb{N}}_0$$
21	20	a1i	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to 2\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(2\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(2\right)=F\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=F\to F\circ g=F\circ F$$
27	26	ad2antrl	$$⊢\left(F\in V\wedge \left(g=F\wedge j=F\right)\right)\to F\circ g=F\circ F$$
28		elex	$$⊢F\in V\to F\in \mathrm{V}$$
29		coexg	$$⊢\left(F\in V\wedge F\in V\right)\to F\circ F\in \mathrm{V}$$
30	29	anidms	$$⊢F\in V\to F\circ F\in \mathrm{V}$$
31	25 27 28 28 30	ovmpod	$$⊢F\in V\to F\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right)F=F\circ F$$
32	31	adantl	$$⊢\left(\mathrm{Rel}F\wedge F\in V\right)\to F\left(g\in \mathrm{V},j\in \mathrm{V}⟼F\circ g\right)F=F\circ F$$
33	3 24 32	3eqtrd	Could not format ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 2 ) = ( F o. F ) ) : No typesetting found for |- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 2 ) = ( F o. F ) ) with typecode |-