Step |
Hyp |
Ref |
Expression |
1 |
|
pthsonfval.v |
|- V = ( Vtx ` G ) |
2 |
1
|
isspthson |
|- ( ( ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) ) |
3 |
2
|
3adantl1 |
|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) ) |
4 |
|
df-spthson |
|- SPathsOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( SPaths ` g ) p ) } ) ) |
5 |
|
spthiswlk |
|- ( f ( SPaths ` G ) p -> f ( Walks ` G ) p ) |
6 |
5
|
adantl |
|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ f ( SPaths ` G ) p ) -> f ( Walks ` G ) p ) |
7 |
1 3 4 6
|
wksonproplem |
|- ( F ( A ( SPathsOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) ) |