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