Metamath Proof Explorer

Theorem wlkonprop

Description: Properties of a walk between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 31-Dec-2020) (Proof shortened by AV, 16-Jan-2021)

Ref Expression
Hypothesis wlkson.v 
|- V = ( Vtx ` G )
Assertion wlkonprop 
|- ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )

Proof

Step Hyp Ref Expression
1 wlkson.v 
 |-  V = ( Vtx ` G )
2 1 fvexi 
 |-  V e. _V
3 df-wlkson 
 |-  WalksOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )
4 1 wlkson 
 |-  ( ( A e. V /\ B e. V ) -> ( A ( WalksOn ` G ) B ) = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) } )
5 4 3adant1 
 |-  ( ( G e. _V /\ A e. V /\ B e. V ) -> ( A ( WalksOn ` G ) B ) = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) } )
6 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
7 6 1 eqtr4di 
 |-  ( g = G -> ( Vtx ` g ) = V )
8 fveq2 
 |-  ( g = G -> ( Walks ` g ) = ( Walks ` G ) )
9 8 breqd 
 |-  ( g = G -> ( f ( Walks ` g ) p <-> f ( Walks ` G ) p ) )
10 9 3anbi1d 
 |-  ( g = G -> ( ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) <-> ( f ( Walks ` G ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) ) )
11 3 5 7 7 10 bropfvvvv 
 |-  ( ( V e. _V /\ V e. _V ) -> ( F ( A ( WalksOn ` G ) B ) P -> ( G e. _V /\ ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) ) )
12 2 2 11 mp2an 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( G e. _V /\ ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) )
13 3anass 
 |-  ( ( G e. _V /\ A e. V /\ B e. V ) <-> ( G e. _V /\ ( A e. V /\ B e. V ) ) )
14 13 anbi1i 
 |-  ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) <-> ( ( G e. _V /\ ( A e. V /\ B e. V ) ) /\ ( F e. _V /\ P e. _V ) ) )
15 df-3an 
 |-  ( ( G e. _V /\ ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) <-> ( ( G e. _V /\ ( A e. V /\ B e. V ) ) /\ ( F e. _V /\ P e. _V ) ) )
16 14 15 bitr4i 
 |-  ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) <-> ( G e. _V /\ ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) )
17 12 16 sylibr 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) )
18 1 iswlkon 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
19 18 3adantl1 
 |-  ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
20 19 biimpd 
 |-  ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( WalksOn ` G ) B ) P -> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
21 20 imdistani 
 |-  ( ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) /\ F ( A ( WalksOn ` G ) B ) P ) -> ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
22 17 21 mpancom 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
23 df-3an 
 |-  ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) <-> ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
24 22 23 sylibr 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )