Metamath Proof Explorer

Theorem 2wlklem

Description: Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018)

Ref Expression
Assertion 2wlklem 
|- ( A. k e. { 0 , 1 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( E ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )

Proof

Step Hyp Ref Expression
1 c0ex 
 |-  0 e. _V
2 1ex 
 |-  1 e. _V
3 2fveq3 
 |-  ( k = 0 -> ( E ` ( F ` k ) ) = ( E ` ( F ` 0 ) ) )
4 fveq2 
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
5 fv0p1e1 
 |-  ( k = 0 -> ( P ` ( k + 1 ) ) = ( P ` 1 ) )
6 4 5 preq12d 
 |-  ( k = 0 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 0 ) , ( P ` 1 ) } )
7 3 6 eqeq12d 
 |-  ( k = 0 -> ( ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
8 2fveq3 
 |-  ( k = 1 -> ( E ` ( F ` k ) ) = ( E ` ( F ` 1 ) ) )
9 fveq2 
 |-  ( k = 1 -> ( P ` k ) = ( P ` 1 ) )
10 oveq1 
 |-  ( k = 1 -> ( k + 1 ) = ( 1 + 1 ) )
11 1p1e2 
 |-  ( 1 + 1 ) = 2
12 10 11 eqtrdi 
 |-  ( k = 1 -> ( k + 1 ) = 2 )
13 12 fveq2d 
 |-  ( k = 1 -> ( P ` ( k + 1 ) ) = ( P ` 2 ) )
14 9 13 preq12d 
 |-  ( k = 1 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 1 ) , ( P ` 2 ) } )
15 8 14 eqeq12d 
 |-  ( k = 1 -> ( ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( E ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
16 1 2 7 15 ralpr 
 |-  ( A. k e. { 0 , 1 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( E ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )