| Step |
Hyp |
Ref |
Expression |
| 1 |
|
2wlkd.p |
|- P = <" A B C "> |
| 2 |
|
2wlkd.f |
|- F = <" J K "> |
| 3 |
|
2wlkd.s |
|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) ) |
| 4 |
|
2wlkd.n |
|- ( ph -> ( A =/= B /\ B =/= C ) ) |
| 5 |
|
2wlkd.e |
|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) ) |
| 6 |
1 2 3 4 5
|
2wlkdlem9 |
|- ( ph -> ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) ) ) |
| 7 |
1 2 3
|
2wlkdlem3 |
|- ( ph -> ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) |
| 8 |
|
preq12 |
|- ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> { ( P ` 0 ) , ( P ` 1 ) } = { A , B } ) |
| 9 |
8
|
3adant3 |
|- ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> { ( P ` 0 ) , ( P ` 1 ) } = { A , B } ) |
| 10 |
9
|
sseq1d |
|- ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) <-> { A , B } C_ ( I ` ( F ` 0 ) ) ) ) |
| 11 |
|
preq12 |
|- ( ( ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> { ( P ` 1 ) , ( P ` 2 ) } = { B , C } ) |
| 12 |
11
|
3adant1 |
|- ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> { ( P ` 1 ) , ( P ` 2 ) } = { B , C } ) |
| 13 |
12
|
sseq1d |
|- ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` ( F ` 1 ) ) <-> { B , C } C_ ( I ` ( F ` 1 ) ) ) ) |
| 14 |
10 13
|
anbi12d |
|- ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` ( F ` 1 ) ) ) <-> ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) ) ) ) |
| 15 |
7 14
|
syl |
|- ( ph -> ( ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` ( F ` 1 ) ) ) <-> ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) ) ) ) |
| 16 |
6 15
|
mpbird |
|- ( ph -> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` ( F ` 1 ) ) ) ) |
| 17 |
1 2
|
2wlkdlem2 |
|- ( 0 ..^ ( # ` F ) ) = { 0 , 1 } |
| 18 |
17
|
raleqi |
|- ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) <-> A. k e. { 0 , 1 } { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) |
| 19 |
|
c0ex |
|- 0 e. _V |
| 20 |
|
1ex |
|- 1 e. _V |
| 21 |
|
fveq2 |
|- ( k = 0 -> ( P ` k ) = ( P ` 0 ) ) |
| 22 |
|
fv0p1e1 |
|- ( k = 0 -> ( P ` ( k + 1 ) ) = ( P ` 1 ) ) |
| 23 |
21 22
|
preq12d |
|- ( k = 0 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 0 ) , ( P ` 1 ) } ) |
| 24 |
|
2fveq3 |
|- ( k = 0 -> ( I ` ( F ` k ) ) = ( I ` ( F ` 0 ) ) ) |
| 25 |
23 24
|
sseq12d |
|- ( k = 0 -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) <-> { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) |
| 26 |
|
fveq2 |
|- ( k = 1 -> ( P ` k ) = ( P ` 1 ) ) |
| 27 |
|
oveq1 |
|- ( k = 1 -> ( k + 1 ) = ( 1 + 1 ) ) |
| 28 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
| 29 |
27 28
|
eqtrdi |
|- ( k = 1 -> ( k + 1 ) = 2 ) |
| 30 |
29
|
fveq2d |
|- ( k = 1 -> ( P ` ( k + 1 ) ) = ( P ` 2 ) ) |
| 31 |
26 30
|
preq12d |
|- ( k = 1 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 1 ) , ( P ` 2 ) } ) |
| 32 |
|
2fveq3 |
|- ( k = 1 -> ( I ` ( F ` k ) ) = ( I ` ( F ` 1 ) ) ) |
| 33 |
31 32
|
sseq12d |
|- ( k = 1 -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) <-> { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` ( F ` 1 ) ) ) ) |
| 34 |
19 20 25 33
|
ralpr |
|- ( A. k e. { 0 , 1 } { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) <-> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` ( F ` 1 ) ) ) ) |
| 35 |
18 34
|
bitri |
|- ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) <-> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` ( F ` 1 ) ) ) ) |
| 36 |
16 35
|
sylibr |
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) |