Theorem itcovalsucov

Description: The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024)

	Ref	Expression
Assertion	itcovalsucov	Could not format assertion : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( F o. G ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		itcovalsuc	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) ) with typecode |-
2		eqidd	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( g e. _V , j e. _V |-> ( F o. g ) ) = ( g e. _V , j e. _V |-> ( F o. g ) ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( g e. _V , j e. _V |-> ( F o. g ) ) = ( g e. _V , j e. _V |-> ( F o. g ) ) ) with typecode |-
3		coeq2	$$⊢g=G\to F\circ g=F\circ G$$
4	3	ad2antrl	Could not format ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ ( g = G /\ j = F ) ) -> ( F o. g ) = ( F o. G ) ) : No typesetting found for |- ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ ( g = G /\ j = F ) ) -> ( F o. g ) = ( F o. G ) ) with typecode |-
5		id	Could not format ( G = ( ( IterComp ` F ) ` Y ) -> G = ( ( IterComp ` F ) ` Y ) ) : No typesetting found for |- ( G = ( ( IterComp ` F ) ` Y ) -> G = ( ( IterComp ` F ) ` Y ) ) with typecode |-
6		fvex	Could not format ( ( IterComp ` F ) ` Y ) e. _V : No typesetting found for |- ( ( IterComp ` F ) ` Y ) e. _V with typecode |-
7	5 6	eqeltrdi	Could not format ( G = ( ( IterComp ` F ) ` Y ) -> G e. _V ) : No typesetting found for |- ( G = ( ( IterComp ` F ) ` Y ) -> G e. _V ) with typecode |-
8	7	eqcoms	Could not format ( ( ( IterComp ` F ) ` Y ) = G -> G e. _V ) : No typesetting found for |- ( ( ( IterComp ` F ) ` Y ) = G -> G e. _V ) with typecode |-
9	8	3ad2ant3	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> G e. _V ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> G e. _V ) with typecode |-
10		elex	$$⊢F\in V\to F\in \mathrm{V}$$
11	10	3ad2ant1	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> F e. _V ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> F e. _V ) with typecode |-
12	8	anim2i	Could not format ( ( F e. V /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F e. V /\ G e. _V ) ) : No typesetting found for |- ( ( F e. V /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F e. V /\ G e. _V ) ) with typecode |-
13	12	3adant2	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F e. V /\ G e. _V ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F e. V /\ G e. _V ) ) with typecode |-
14		coexg	$$⊢\left(F\in V\wedge G\in \mathrm{V}\right)\to F\circ G\in \mathrm{V}$$
15	13 14	syl	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F o. G ) e. _V ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( F o. G ) e. _V ) with typecode |-
16	2 4 9 11 15	ovmpod	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. G ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. G ) ) with typecode |-
17	1 16	eqtrd	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( F o. G ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( F o. G ) ) with typecode |-