Metamath Proof Explorer

Theorem spthdifv

Description: The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018) (Revised by AV, 5-Jun-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion spthdifv 
|- ( F ( SPaths ` G ) P -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )

Proof

Step Hyp Ref Expression
1 isspth 
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
2 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
5 df-f1 
 |-  ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) <-> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' P ) )
6 5 simplbi2 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( Fun `' P -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) )
7 2 4 6 3syl 
 |-  ( F ( Trails ` G ) P -> ( Fun `' P -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) )
8 7 imp 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )
9 1 8 sylbi 
 |-  ( F ( SPaths ` G ) P -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )