Metamath Proof Explorer

Theorem usgr2wlkspth

Description: In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 27-Jan-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Assertion usgr2wlkspth 
|- ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P <-> F ( A ( SPathsOn ` G ) B ) P ) )

Proof

Step Hyp Ref Expression
1 simpl31 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> F ( Walks ` G ) P )
2 simp2 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` 0 ) = A )
3 simp3 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` ( # ` F ) ) = B )
4 2 3 neeq12d 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> A =/= B ) )
5 4 bicomd 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( A =/= B <-> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
6 5 3anbi3d 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) <-> ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) )
7 usgr2wlkspthlem1 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' F )
8 7 ex 
 |-  ( F ( Walks ` G ) P -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> Fun `' F ) )
9 8 3ad2ant1 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> Fun `' F ) )
10 6 9 sylbid 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> Fun `' F ) )
11 10 3ad2ant3 
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> Fun `' F ) )
12 11 imp 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> Fun `' F )
13 istrl 
 |-  ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) )
14 1 12 13 sylanbrc 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> F ( Trails ` G ) P )
15 usgr2wlkspthlem2 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' P )
16 15 ex 
 |-  ( F ( Walks ` G ) P -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> Fun `' P ) )
17 16 3ad2ant1 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> Fun `' P ) )
18 6 17 sylbid 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> Fun `' P ) )
19 18 3ad2ant3 
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> Fun `' P ) )
20 19 imp 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> Fun `' P )
21 isspth 
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
22 14 20 21 sylanbrc 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> F ( SPaths ` G ) P )
23 3simpc 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
24 23 3ad2ant3 
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
25 24 adantr 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
26 3anass 
 |-  ( ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) <-> ( F ( SPaths ` G ) P /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
27 22 25 26 sylanbrc 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
28 3simpa 
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
29 28 adantr 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
30 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
31 30 isspthonpth 
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
32 29 31 syl 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
33 27 32 mpbird 
 |-  ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) ) -> F ( A ( SPathsOn ` G ) B ) P )
34 33 ex 
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> F ( A ( SPathsOn ` G ) B ) P ) )
35 30 wlkonprop 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
36 3simpc 
 |-  ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
37 36 3anim1i 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
38 35 37 syl 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
39 34 38 syl11 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P -> F ( A ( SPathsOn ` G ) B ) P ) )
40 spthonpthon 
 |-  ( F ( A ( SPathsOn ` G ) B ) P -> F ( A ( PathsOn ` G ) B ) P )
41 pthontrlon 
 |-  ( F ( A ( PathsOn ` G ) B ) P -> F ( A ( TrailsOn ` G ) B ) P )
42 trlsonwlkon 
 |-  ( F ( A ( TrailsOn ` G ) B ) P -> F ( A ( WalksOn ` G ) B ) P )
43 40 41 42 3syl 
 |-  ( F ( A ( SPathsOn ` G ) B ) P -> F ( A ( WalksOn ` G ) B ) P )
44 39 43 impbid1 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P <-> F ( A ( SPathsOn ` G ) B ) P ) )