Metamath Proof Explorer

Theorem pthdifv

Description: The vertices of a path are distinct (except the first and last vertex), so the restricted vertex function is one-to-one. (Contributed by AV, 2-Oct-2025)

Ref Expression
Assertion pthdifv 
|- ( F ( Paths ` G ) P -> ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )

Proof

Step Hyp Ref Expression
1 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
4 fz1ssfz0 
 |-  ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
5 4 a1i 
 |-  ( F ( Walks ` G ) P -> ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) )
6 3 5 fssresd 
 |-  ( F ( Walks ` G ) P -> ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) )
7 1 6 syl 
 |-  ( F ( Trails ` G ) P -> ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) )
8 7 anim1i 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) -> ( ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) )
9 8 3adant3 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) )
10 dfpth2 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )
11 df-f1 
 |-  ( ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) <-> ( ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) )
12 9 10 11 3imtr4i 
 |-  ( F ( Paths ` G ) P -> ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )