Description: Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017) (Revised by AV, 7-Jan-2021) (Proof shortened by AV, 16-Jan-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | trlsonfval.v | |- V = ( Vtx ` G ) |
|
| Assertion | trlsonprop | |- ( F ( A ( TrailsOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trlsonfval.v | |- V = ( Vtx ` G ) |
|
| 2 | 1 | istrlson | |- ( ( ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) ) |
| 3 | 2 | 3adantl1 | |- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) ) |
| 4 | df-trlson | |- TrailsOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( WalksOn ` g ) b ) p /\ f ( Trails ` g ) p ) } ) ) |
|
| 5 | 1 3 4 | wksonproplem | |- ( F ( A ( TrailsOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) ) |