Metamath Proof Explorer

Theorem isspthonpth

Description: A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 17-Jan-2021)

Ref Expression
Hypothesis isspthonpth.v 
|- V = ( Vtx ` G )
Assertion isspthonpth 
|- ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )

Proof

Step Hyp Ref Expression
1 isspthonpth.v 
 |-  V = ( Vtx ` G )
2 1 isspthson 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) )
3 1 istrlson 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )
4 3 adantr 
 |-  ( ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) /\ F ( SPaths ` G ) P ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )
5 spthispth 
 |-  ( F ( SPaths ` G ) P -> F ( Paths ` G ) P )
6 pthistrl 
 |-  ( F ( Paths ` G ) P -> F ( Trails ` G ) P )
7 5 6 syl 
 |-  ( F ( SPaths ` G ) P -> F ( Trails ` G ) P )
8 7 adantl 
 |-  ( ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) /\ F ( SPaths ` G ) P ) -> F ( Trails ` G ) P )
9 8 biantrud 
 |-  ( ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) /\ F ( SPaths ` G ) P ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )
10 spthiswlk 
 |-  ( F ( SPaths ` G ) P -> F ( Walks ` G ) P )
11 10 adantl 
 |-  ( ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) /\ F ( SPaths ` G ) P ) -> F ( Walks ` G ) P )
12 1 iswlkon 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
13 3anass 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) <-> ( F ( Walks ` G ) P /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
14 12 13 bitrdi 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) )
15 14 adantr 
 |-  ( ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) /\ F ( SPaths ` G ) P ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) )
16 11 15 mpbirand 
 |-  ( ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) /\ F ( SPaths ` G ) P ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
17 4 9 16 3bitr2d 
 |-  ( ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) /\ F ( SPaths ` G ) P ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
18 17 ex 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( SPaths ` G ) P -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) )
19 18 pm5.32rd 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) <-> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) /\ F ( SPaths ` G ) P ) ) )
20 3anass 
 |-  ( ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) <-> ( F ( SPaths ` G ) P /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
21 ancom 
 |-  ( ( F ( SPaths ` G ) P /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) <-> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) /\ F ( SPaths ` G ) P ) )
22 20 21 bitr2i 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) /\ F ( SPaths ` G ) P ) <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
23 19 22 bitrdi 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
24 2 23 bitrd 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )