Step |
Hyp |
Ref |
Expression |
1 |
|
3wlkd.p |
|- P = <" A B C D "> |
2 |
|
3wlkd.f |
|- F = <" J K L "> |
3 |
|
3wlkd.s |
|- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) ) |
4 |
|
3wlkd.n |
|- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) |
5 |
|
3wlkd.e |
|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) ) |
6 |
|
3wlkd.v |
|- V = ( Vtx ` G ) |
7 |
|
3wlkd.i |
|- I = ( iEdg ` G ) |
8 |
|
3trld.n |
|- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) ) |
9 |
1 2 3 4 5 6 7 8
|
3trlond |
|- ( ph -> F ( A ( TrailsOn ` G ) D ) P ) |
10 |
1 2 3 4 5 6 7 8
|
3pthd |
|- ( ph -> F ( Paths ` G ) P ) |
11 |
3
|
simplld |
|- ( ph -> A e. V ) |
12 |
3
|
simprrd |
|- ( ph -> D e. V ) |
13 |
|
s3cli |
|- <" J K L "> e. Word _V |
14 |
2 13
|
eqeltri |
|- F e. Word _V |
15 |
|
s4cli |
|- <" A B C D "> e. Word _V |
16 |
1 15
|
eqeltri |
|- P e. Word _V |
17 |
14 16
|
pm3.2i |
|- ( F e. Word _V /\ P e. Word _V ) |
18 |
17
|
a1i |
|- ( ph -> ( F e. Word _V /\ P e. Word _V ) ) |
19 |
6
|
ispthson |
|- ( ( ( A e. V /\ D e. V ) /\ ( F e. Word _V /\ P e. Word _V ) ) -> ( F ( A ( PathsOn ` G ) D ) P <-> ( F ( A ( TrailsOn ` G ) D ) P /\ F ( Paths ` G ) P ) ) ) |
20 |
11 12 18 19
|
syl21anc |
|- ( ph -> ( F ( A ( PathsOn ` G ) D ) P <-> ( F ( A ( TrailsOn ` G ) D ) P /\ F ( Paths ` G ) P ) ) ) |
21 |
9 10 20
|
mpbir2and |
|- ( ph -> F ( A ( PathsOn ` G ) D ) P ) |