| Step |
Hyp |
Ref |
Expression |
| 1 |
|
wlkiswwlks2lem.f |
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) ) |
| 2 |
|
fveq2 |
|- ( x = I -> ( P ` x ) = ( P ` I ) ) |
| 3 |
|
fvoveq1 |
|- ( x = I -> ( P ` ( x + 1 ) ) = ( P ` ( I + 1 ) ) ) |
| 4 |
2 3
|
preq12d |
|- ( x = I -> { ( P ` x ) , ( P ` ( x + 1 ) ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) |
| 5 |
4
|
fveq2d |
|- ( x = I -> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) |
| 6 |
|
simpr |
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) |
| 7 |
|
fvexd |
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) e. _V ) |
| 8 |
1 5 6 7
|
fvmptd3 |
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) |