Metamath Proof Explorer


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 0 = 0
5 1nn0 1 0
6 5 a1i Rel F F V 1 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 Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 1 = F
13 eqidd Rel F F V i 0 if i = 0 I dom F F = i 0 if i = 0 I dom F F
14 2ne0 2 0
15 neeq1 i = 2 i 0 2 0
16 14 15 mpbiri i = 2 i 0
17 16 neneqd i = 2 ¬ i = 0
18 17 iffalsed i = 2 if i = 0 I dom F F = F
19 18 adantl Rel F F V i = 2 if i = 0 I dom F F = F
20 2nn0 2 0
21 20 a1i Rel F F V 2 0
22 simpr Rel F F V F V
23 13 19 21 22 fvmptd Rel F F V i 0 if i = 0 I dom F F 2 = F
24 4 6 7 12 23 seqp1d Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 2 = F g V , j V F g F
25 eqidd F V g V , j V F g = g V , j V F g
26 coeq2 g = F F g = F F
27 26 ad2antrl F V g = F j = F F g = F F
28 elex F V F V
29 coexg F V F V F F V
30 29 anidms F V F F V
31 25 27 28 28 30 ovmpod F V F g V , j V F g F = F F
32 31 adantl Rel F F V F g V , j V F g F = F 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 |-