Metamath Proof Explorer

Theorem istrlson

Description: Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypothesis trlsonfval.v 
|- V = ( Vtx ` G )
Assertion istrlson 
|- ( ( ( A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )

Proof

Step Hyp Ref Expression
1 trlsonfval.v 
 |-  V = ( Vtx ` G )
2 1 trlsonfval 
 |-  ( ( A e. V /\ B e. V ) -> ( A ( TrailsOn ` G ) B ) = { <. f , p >. | ( f ( A ( WalksOn ` G ) B ) p /\ f ( Trails ` G ) p ) } )
3 2 breqd 
 |-  ( ( A e. V /\ B e. V ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> F { <. f , p >. | ( f ( A ( WalksOn ` G ) B ) p /\ f ( Trails ` G ) p ) } P ) )
4 breq12 
 |-  ( ( f = F /\ p = P ) -> ( f ( A ( WalksOn ` G ) B ) p <-> F ( A ( WalksOn ` G ) B ) P ) )
5 breq12 
 |-  ( ( f = F /\ p = P ) -> ( f ( Trails ` G ) p <-> F ( Trails ` G ) P ) )
6 4 5 anbi12d 
 |-  ( ( f = F /\ p = P ) -> ( ( f ( A ( WalksOn ` G ) B ) p /\ f ( Trails ` G ) p ) <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )
7 eqid 
 |-  { <. f , p >. | ( f ( A ( WalksOn ` G ) B ) p /\ f ( Trails ` G ) p ) } = { <. f , p >. | ( f ( A ( WalksOn ` G ) B ) p /\ f ( Trails ` G ) p ) }
8 6 7 brabga 
 |-  ( ( F e. U /\ P e. Z ) -> ( F { <. f , p >. | ( f ( A ( WalksOn ` G ) B ) p /\ f ( Trails ` G ) p ) } P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )
9 3 8 sylan9bb 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )