This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iswlkon

Description: Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017) (Revised by AV, 31-Dec-2020) (Revised by AV, 22-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 wlkson.v 
 |-  V = ( Vtx ` G )
2 1 wlkson 
 |-  ( ( A e. V /\ B e. V ) -> ( A ( WalksOn ` G ) B ) = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) } )
3 fveq1 
 |-  ( p = P -> ( p ` 0 ) = ( P ` 0 ) )
4 3 adantl 
 |-  ( ( f = F /\ p = P ) -> ( p ` 0 ) = ( P ` 0 ) )
5 4 eqeq1d 
 |-  ( ( f = F /\ p = P ) -> ( ( p ` 0 ) = A <-> ( P ` 0 ) = A ) )
6 simpr 
 |-  ( ( f = F /\ p = P ) -> p = P )
7 fveq2 
 |-  ( f = F -> ( # ` f ) = ( # ` F ) )
8 7 adantr 
 |-  ( ( f = F /\ p = P ) -> ( # ` f ) = ( # ` F ) )
9 6 8 fveq12d 
 |-  ( ( f = F /\ p = P ) -> ( p ` ( # ` f ) ) = ( P ` ( # ` F ) ) )
10 9 eqeq1d 
 |-  ( ( f = F /\ p = P ) -> ( ( p ` ( # ` f ) ) = B <-> ( P ` ( # ` F ) ) = B ) )
11 2 5 10 2rbropap 
 |-  ( ( ( A e. V /\ B e. V ) /\ F e. U /\ P e. Z ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
12 11 3expb 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )