Theorem itcovalsuc

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	itcovalsuc	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		simp1	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 |-
2		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 |-
3	2	fveq1d	Could not format ( F e. V -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` ( Y + 1 ) ) ) : No typesetting found for |- ( F e. V -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` ( Y + 1 ) ) ) with typecode |-
4	1 3	syl	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` ( Y + 1 ) ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` ( Y + 1 ) ) ) with typecode |-
5		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
6		simp2	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> Y e. NN0 ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> Y e. NN0 ) with typecode |-
7		eqid	$$⊢Y+1=Y+1$$
8	2	adantr	Could not format ( ( F e. V /\ Y e. NN0 ) -> ( 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 /\ Y e. NN0 ) -> ( 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 |-
9	8	fveq1d	Could not format ( ( F e. V /\ Y e. NN0 ) -> ( ( IterComp ` F ) ` Y ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 ) -> ( ( IterComp ` F ) ` Y ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) ) with typecode |-
10	9	eqeq1d	Could not format ( ( F e. V /\ Y e. NN0 ) -> ( ( ( IterComp ` F ) ` Y ) = G <-> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) = G ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 ) -> ( ( ( IterComp ` F ) ` Y ) = G <-> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) = G ) ) with typecode |-
11	10	biimp3a	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) = G ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) = G ) with typecode |-
12		eqidd	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) = ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) = ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) with typecode |-
13		nn0p1gt0	$$⊢Y\in {\mathbb{N}}_0\to 0<Y+1$$
14	13	3ad2ant2	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> 0 < ( Y + 1 ) ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> 0 < ( Y + 1 ) ) with typecode |-
15	14	gt0ne0d	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( Y + 1 ) =/= 0 ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( Y + 1 ) =/= 0 ) with typecode |-
16	15	adantr	Could not format ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> ( Y + 1 ) =/= 0 ) : No typesetting found for |- ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> ( Y + 1 ) =/= 0 ) with typecode |-
17		neeq1	$$⊢i=Y+1\to \left(i\ne 0\leftrightarrow Y+1\ne 0\right)$$
18	17	adantl	Could not format ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> ( i =/= 0 <-> ( Y + 1 ) =/= 0 ) ) : No typesetting found for |- ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> ( i =/= 0 <-> ( Y + 1 ) =/= 0 ) ) with typecode |-
19	16 18	mpbird	Could not format ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> i =/= 0 ) : No typesetting found for |- ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> i =/= 0 ) with typecode |-
20	19	neneqd	Could not format ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> -. i = 0 ) : No typesetting found for |- ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> -. i = 0 ) with typecode |-
21	20	iffalsed	Could not format ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> if ( i = 0 , ( _I |` dom F ) , F ) = F ) : No typesetting found for |- ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> if ( i = 0 , ( _I |` dom F ) , F ) = F ) with typecode |-
22		peano2nn0	$$⊢Y\in {\mathbb{N}}_0\to Y+1\in {\mathbb{N}}_0$$
23	22	3ad2ant2	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( Y + 1 ) e. NN0 ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( Y + 1 ) e. NN0 ) with typecode |-
24	12 21 23 1	fvmptd	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ` ( Y + 1 ) ) = F ) : No typesetting found for |- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ` ( Y + 1 ) ) = F ) with typecode |-
25	5 6 7 11 24	seqp1d	Could not format ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , 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 ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` ( Y + 1 ) ) = ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) ) with typecode |-
26	4 25	eqtrd	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 |-