Metamath Proof Explorer

Theorem trlsonprop

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

Proof

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 trliswlk 
 |-  ( f ( Trails ` G ) p -> f ( Walks ` G ) p )
6 5 adantl 
 |-  ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ f ( Trails ` G ) p ) -> f ( Walks ` G ) p )
7 1 3 4 6 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 ) ) )