Step |
Hyp |
Ref |
Expression |
1 |
|
itcoval |
|- ( 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 ) ) ) ) |
2 |
1
|
fveq1d |
|- ( F e. V -> ( ( IterComp ` F ) ` 1 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) ) |
3 |
2
|
adantl |
|- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) ) |
4 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
5 |
|
0nn0 |
|- 0 e. NN0 |
6 |
5
|
a1i |
|- ( ( Rel F /\ F e. V ) -> 0 e. NN0 ) |
7 |
|
1e0p1 |
|- 1 = ( 0 + 1 ) |
8 |
1
|
eqcomd |
|- ( 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 ) ) |
9 |
8
|
fveq1d |
|- ( F e. V -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 0 ) = ( ( IterComp ` F ) ` 0 ) ) |
10 |
|
itcoval0 |
|- ( F e. V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom F ) ) |
11 |
9 10
|
eqtrd |
|- ( F e. V -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 0 ) = ( _I |` dom F ) ) |
12 |
11
|
adantl |
|- ( ( 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 ) ) ) ` 0 ) = ( _I |` dom F ) ) |
13 |
|
eqidd |
|- ( ( Rel F /\ F e. V ) -> ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) = ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) |
14 |
|
ax-1ne0 |
|- 1 =/= 0 |
15 |
14
|
neii |
|- -. 1 = 0 |
16 |
|
eqeq1 |
|- ( i = 1 -> ( i = 0 <-> 1 = 0 ) ) |
17 |
15 16
|
mtbiri |
|- ( i = 1 -> -. i = 0 ) |
18 |
17
|
iffalsed |
|- ( i = 1 -> if ( i = 0 , ( _I |` dom F ) , F ) = F ) |
19 |
18
|
adantl |
|- ( ( ( Rel F /\ F e. V ) /\ i = 1 ) -> if ( i = 0 , ( _I |` dom F ) , F ) = F ) |
20 |
|
1nn0 |
|- 1 e. NN0 |
21 |
20
|
a1i |
|- ( ( Rel F /\ F e. V ) -> 1 e. NN0 ) |
22 |
|
simpr |
|- ( ( Rel F /\ F e. V ) -> F e. V ) |
23 |
13 19 21 22
|
fvmptd |
|- ( ( Rel F /\ F e. V ) -> ( ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ` 1 ) = F ) |
24 |
4 6 7 12 23
|
seqp1d |
|- ( ( 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 ) = ( ( _I |` dom F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) ) |
25 |
|
eqidd |
|- ( F e. V -> ( g e. _V , j e. _V |-> ( F o. g ) ) = ( g e. _V , j e. _V |-> ( F o. g ) ) ) |
26 |
|
coeq2 |
|- ( g = ( _I |` dom F ) -> ( F o. g ) = ( F o. ( _I |` dom F ) ) ) |
27 |
26
|
ad2antrl |
|- ( ( F e. V /\ ( g = ( _I |` dom F ) /\ j = F ) ) -> ( F o. g ) = ( F o. ( _I |` dom F ) ) ) |
28 |
|
dmexg |
|- ( F e. V -> dom F e. _V ) |
29 |
28
|
resiexd |
|- ( F e. V -> ( _I |` dom F ) e. _V ) |
30 |
|
elex |
|- ( F e. V -> F e. _V ) |
31 |
|
coexg |
|- ( ( F e. V /\ ( _I |` dom F ) e. _V ) -> ( F o. ( _I |` dom F ) ) e. _V ) |
32 |
29 31
|
mpdan |
|- ( F e. V -> ( F o. ( _I |` dom F ) ) e. _V ) |
33 |
25 27 29 30 32
|
ovmpod |
|- ( F e. V -> ( ( _I |` dom F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. ( _I |` dom F ) ) ) |
34 |
33
|
adantl |
|- ( ( Rel F /\ F e. V ) -> ( ( _I |` dom F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. ( _I |` dom F ) ) ) |
35 |
|
coires1 |
|- ( F o. ( _I |` dom F ) ) = ( F |` dom F ) |
36 |
|
resdm |
|- ( Rel F -> ( F |` dom F ) = F ) |
37 |
36
|
adantr |
|- ( ( Rel F /\ F e. V ) -> ( F |` dom F ) = F ) |
38 |
35 37
|
syl5eq |
|- ( ( Rel F /\ F e. V ) -> ( F o. ( _I |` dom F ) ) = F ) |
39 |
34 38
|
eqtrd |
|- ( ( Rel F /\ F e. V ) -> ( ( _I |` dom F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = F ) |
40 |
24 39
|
eqtrd |
|- ( ( 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 ) = F ) |
41 |
3 40
|
eqtrd |
|- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = F ) |