Metamath Proof Explorer


Theorem wlkiswwlks2lem2

Description: Lemma 2 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)

Ref Expression
Hypothesis wlkiswwlks2lem.f
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )
Assertion wlkiswwlks2lem2
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )

Proof

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 ) ) } ) )