Metamath Proof Explorer

Theorem wlkson

Description: The set of walks between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 30-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypothesis wlkson.v 
|- V = ( Vtx ` G )
Assertion wlkson 
|- ( ( A e. V /\ B e. V ) -> ( A ( WalksOn ` G ) B ) = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) } )

Proof

Step Hyp Ref Expression
1 wlkson.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 simpr 
 |-  ( ( ( A e. V /\ B e. V ) /\ f ( Walks ` G ) p ) -> f ( Walks ` G ) p )
11 eqeq2 
 |-  ( a = A -> ( ( p ` 0 ) = a <-> ( p ` 0 ) = A ) )
12 eqeq2 
 |-  ( b = B -> ( ( p ` ( # ` f ) ) = b <-> ( p ` ( # ` f ) ) = B ) )
13 11 12 bi2anan9 
 |-  ( ( a = A /\ b = B ) -> ( ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) <-> ( ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) ) )
14 biidd 
 |-  ( g = G -> ( ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) <-> ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) ) )
15 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 ) } ) )
16 eqid 
 |-  ( Vtx ` g ) = ( Vtx ` g )
17 3anass 
 |-  ( ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) <-> ( f ( Walks ` g ) p /\ ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) ) )
18 17 biancomi 
 |-  ( ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) <-> ( ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) /\ f ( Walks ` g ) p ) )
19 18 opabbii 
 |-  { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } = { <. f , p >. | ( ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) /\ f ( Walks ` g ) p ) }
20 16 16 19 mpoeq123i 
 |-  ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) = ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) /\ f ( Walks ` g ) p ) } )
21 20 mpteq2i 
 |-  ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) ) = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) /\ f ( Walks ` g ) p ) } ) )
22 15 21 eqtri 
 |-  WalksOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( ( ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) /\ f ( Walks ` g ) p ) } ) )
23 3 5 7 9 10 13 14 22 mptmpoopabbrd 
 |-  ( ( A e. V /\ B e. V ) -> ( A ( WalksOn ` G ) B ) = { <. f , p >. | ( ( ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) /\ f ( Walks ` G ) p ) } )
24 ancom 
 |-  ( ( ( ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) /\ f ( Walks ` G ) p ) <-> ( f ( Walks ` G ) p /\ ( ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) ) )
25 3anass 
 |-  ( ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) <-> ( f ( Walks ` G ) p /\ ( ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) ) )
26 24 25 bitr4i 
 |-  ( ( ( ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) /\ f ( Walks ` G ) p ) <-> ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) )
27 26 opabbii 
 |-  { <. f , p >. | ( ( ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) /\ f ( Walks ` G ) p ) } = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) }
28 23 27 eqtrdi 
 |-  ( ( A e. V /\ B e. V ) -> ( A ( WalksOn ` G ) B ) = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) } )