Theorem itcoval3

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

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