Metamath Proof Explorer

Theorem uhgrwkspth

Description: Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021) (Proof shortened by AV, 31-Oct-2021) (Revised by AV, 7-Jul-2022)

Ref Expression
Assertion uhgrwkspth 
|- ( ( G e. W /\ ( # ` F ) = 1 /\ 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( Walks ` G ) P )
2 uhgrwkspthlem1 
 |-  ( ( F ( Walks ` G ) P /\ ( # ` F ) = 1 ) -> Fun `' F )
3 2 expcom 
 |-  ( ( # ` F ) = 1 -> ( F ( Walks ` G ) P -> Fun `' F ) )
4 3 3ad2ant2 
 |-  ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( Walks ` G ) P -> Fun `' F ) )
5 4 com12 
 |-  ( F ( Walks ` G ) P -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) )
6 5 3ad2ant1 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) )
7 6 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. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) )
8 7 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> Fun `' F )
9 istrl 
 |-  ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) )
10 1 8 9 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( Trails ` G ) P )
11 3simpc 
 |-  ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( ( # ` F ) = 1 /\ A =/= B ) )
12 11 adantl 
 |-  ( ( ( ( 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( # ` F ) = 1 /\ A =/= B ) )
13 3simpc 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
14 13 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 ) )
15 14 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
16 uhgrwkspthlem2 
 |-  ( ( F ( Walks ` G ) P /\ ( ( # ` F ) = 1 /\ A =/= B ) /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> Fun `' P )
17 1 12 15 16 syl3anc 
 |-  ( ( ( ( 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> Fun `' P )
18 isspth 
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
19 10 17 18 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( SPaths ` G ) P )
20 3anass 
 |-  ( ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) <-> ( F ( SPaths ` G ) P /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
21 19 15 20 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) )
22 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 ) ) )
23 22 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
24 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
25 24 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 ) ) )
26 23 25 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
27 21 26 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. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( A ( SPathsOn ` G ) B ) P )
28 27 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. W /\ ( # ` F ) = 1 /\ A =/= B ) -> F ( A ( SPathsOn ` G ) B ) P ) )
29 24 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 ) ) )
30 3simpc 
 |-  ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
31 30 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 ) ) )
32 29 31 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 ) ) )
33 28 32 syl11 
 |-  ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P -> F ( A ( SPathsOn ` G ) B ) P ) )
34 spthonpthon 
 |-  ( F ( A ( SPathsOn ` G ) B ) P -> F ( A ( PathsOn ` G ) B ) P )
35 pthontrlon 
 |-  ( F ( A ( PathsOn ` G ) B ) P -> F ( A ( TrailsOn ` G ) B ) P )
36 trlsonwlkon 
 |-  ( F ( A ( TrailsOn ` G ) B ) P -> F ( A ( WalksOn ` G ) B ) P )
37 34 35 36 3syl 
 |-  ( F ( A ( SPathsOn ` G ) B ) P -> F ( A ( WalksOn ` G ) B ) P )
38 33 37 impbid1 
 |-  ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P <-> F ( A ( SPathsOn ` G ) B ) P ) )