Metamath Proof Explorer


Theorem pthsonfval

Description: The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 16-Jan-2021) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypothesis pthsonfval.v
|- V = ( Vtx ` G )
Assertion pthsonfval
|- ( ( A e. V /\ B e. V ) -> ( A ( PathsOn ` G ) B ) = { <. f , p >. | ( f ( A ( TrailsOn ` G ) B ) p /\ f ( Paths ` G ) p ) } )

Proof

Step Hyp Ref Expression
1 pthsonfval.v
 |-  V = ( Vtx ` G )
2 1 1vgrex
 |-  ( A e. V -> G e. _V )
3 2 adantr
 |-  ( ( A e. V /\ B e. V ) -> G e. _V )
4 simpl
 |-  ( ( A e. V /\ B e. V ) -> A e. V )
5 4 1 eleqtrdi
 |-  ( ( A e. V /\ B e. V ) -> A e. ( Vtx ` G ) )
6 simpr
 |-  ( ( A e. V /\ B e. V ) -> B e. V )
7 6 1 eleqtrdi
 |-  ( ( A e. V /\ B e. V ) -> B e. ( Vtx ` G ) )
8 wksv
 |-  { <. f , p >. | f ( Walks ` G ) p } e. _V
9 8 a1i
 |-  ( ( A e. V /\ B e. V ) -> { <. f , p >. | f ( Walks ` G ) p } e. _V )
10 pthiswlk
 |-  ( f ( Paths ` G ) p -> f ( Walks ` G ) p )
11 10 adantl
 |-  ( ( ( A e. V /\ B e. V ) /\ f ( Paths ` G ) p ) -> f ( Walks ` G ) p )
12 df-pthson
 |-  PathsOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( Paths ` g ) p ) } ) )
13 3 5 7 9 11 12 mptmpoopabovd
 |-  ( ( A e. V /\ B e. V ) -> ( A ( PathsOn ` G ) B ) = { <. f , p >. | ( f ( A ( TrailsOn ` G ) B ) p /\ f ( Paths ` G ) p ) } )