Metamath Proof Explorer

Theorem isspthson

Description: Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 16-Jan-2021) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypothesis pthsonfval.v 
|- V = ( Vtx ` G )
Assertion isspthson 
|- ( ( ( A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) )

Proof

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