Metamath Proof Explorer

Theorem 1pthond

Description: In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021) (Revised by AV, 23-Mar-2021)

Ref Expression
Hypotheses 1wlkd.p 
|- P = <" X Y ">
1wlkd.f 
|- F = <" J ">
1wlkd.x 
|- ( ph -> X e. V )
1wlkd.y 
|- ( ph -> Y e. V )
1wlkd.l 
|- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
1wlkd.j 
|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
1wlkd.v 
|- V = ( Vtx ` G )
1wlkd.i 
|- I = ( iEdg ` G )
Assertion 1pthond 
|- ( ph -> F ( X ( PathsOn ` G ) Y ) P )

Proof

Step Hyp Ref Expression
1 1wlkd.p 
 |-  P = <" X Y ">
2 1wlkd.f 
 |-  F = <" J ">
3 1wlkd.x 
 |-  ( ph -> X e. V )
4 1wlkd.y 
 |-  ( ph -> Y e. V )
5 1wlkd.l 
 |-  ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
6 1wlkd.j 
 |-  ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
7 1wlkd.v 
 |-  V = ( Vtx ` G )
8 1wlkd.i 
 |-  I = ( iEdg ` G )
9 1 2 3 4 5 6 7 8 1wlkd 
 |-  ( ph -> F ( Walks ` G ) P )
10 1 fveq1i 
 |-  ( P ` 0 ) = ( <" X Y "> ` 0 )
11 s2fv0 
 |-  ( X e. V -> ( <" X Y "> ` 0 ) = X )
12 10 11 syl5eq 
 |-  ( X e. V -> ( P ` 0 ) = X )
13 3 12 syl 
 |-  ( ph -> ( P ` 0 ) = X )
14 2 fveq2i 
 |-  ( # ` F ) = ( # ` <" J "> )
15 s1len 
 |-  ( # ` <" J "> ) = 1
16 14 15 eqtri 
 |-  ( # ` F ) = 1
17 1 16 fveq12i 
 |-  ( P ` ( # ` F ) ) = ( <" X Y "> ` 1 )
18 s2fv1 
 |-  ( Y e. V -> ( <" X Y "> ` 1 ) = Y )
19 4 18 syl 
 |-  ( ph -> ( <" X Y "> ` 1 ) = Y )
20 17 19 syl5eq 
 |-  ( ph -> ( P ` ( # ` F ) ) = Y )
21 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
22 3simpc 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F e. _V /\ P e. _V ) )
23 9 21 22 3syl 
 |-  ( ph -> ( F e. _V /\ P e. _V ) )
24 3 4 23 jca31 
 |-  ( ph -> ( ( X e. V /\ Y e. V ) /\ ( F e. _V /\ P e. _V ) ) )
25 7 iswlkon 
 |-  ( ( ( X e. V /\ Y e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( X ( WalksOn ` G ) Y ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = X /\ ( P ` ( # ` F ) ) = Y ) ) )
26 24 25 syl 
 |-  ( ph -> ( F ( X ( WalksOn ` G ) Y ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = X /\ ( P ` ( # ` F ) ) = Y ) ) )
27 9 13 20 26 mpbir3and 
 |-  ( ph -> F ( X ( WalksOn ` G ) Y ) P )
28 1 2 3 4 5 6 7 8 1trld 
 |-  ( ph -> F ( Trails ` G ) P )
29 7 istrlson 
 |-  ( ( ( X e. V /\ Y e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( X ( TrailsOn ` G ) Y ) P <-> ( F ( X ( WalksOn ` G ) Y ) P /\ F ( Trails ` G ) P ) ) )
30 24 29 syl 
 |-  ( ph -> ( F ( X ( TrailsOn ` G ) Y ) P <-> ( F ( X ( WalksOn ` G ) Y ) P /\ F ( Trails ` G ) P ) ) )
31 27 28 30 mpbir2and 
 |-  ( ph -> F ( X ( TrailsOn ` G ) Y ) P )
32 1 2 3 4 5 6 7 8 1pthd 
 |-  ( ph -> F ( Paths ` G ) P )
33 3 adantl 
 |-  ( ( ( F e. _V /\ P e. _V ) /\ ph ) -> X e. V )
34 4 adantl 
 |-  ( ( ( F e. _V /\ P e. _V ) /\ ph ) -> Y e. V )
35 simpl 
 |-  ( ( ( F e. _V /\ P e. _V ) /\ ph ) -> ( F e. _V /\ P e. _V ) )
36 33 34 35 jca31 
 |-  ( ( ( F e. _V /\ P e. _V ) /\ ph ) -> ( ( X e. V /\ Y e. V ) /\ ( F e. _V /\ P e. _V ) ) )
37 36 ex 
 |-  ( ( F e. _V /\ P e. _V ) -> ( ph -> ( ( X e. V /\ Y e. V ) /\ ( F e. _V /\ P e. _V ) ) ) )
38 21 22 37 3syl 
 |-  ( F ( Walks ` G ) P -> ( ph -> ( ( X e. V /\ Y e. V ) /\ ( F e. _V /\ P e. _V ) ) ) )
39 9 38 mpcom 
 |-  ( ph -> ( ( X e. V /\ Y e. V ) /\ ( F e. _V /\ P e. _V ) ) )
40 7 ispthson 
 |-  ( ( ( X e. V /\ Y e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( X ( PathsOn ` G ) Y ) P <-> ( F ( X ( TrailsOn ` G ) Y ) P /\ F ( Paths ` G ) P ) ) )
41 39 40 syl 
 |-  ( ph -> ( F ( X ( PathsOn ` G ) Y ) P <-> ( F ( X ( TrailsOn ` G ) Y ) P /\ F ( Paths ` G ) P ) ) )
42 31 32 41 mpbir2and 
 |-  ( ph -> F ( X ( PathsOn ` G ) Y ) P )