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