Metamath Proof Explorer

Theorem pthonpth

Description: A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021)

Ref Expression
Assertion pthonpth 
|- ( F ( Paths ` G ) P -> F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` ( # ` F ) ) ) P )

Proof

Step Hyp Ref Expression
1 pthistrl 
 |-  ( F ( Paths ` G ) P -> F ( Trails ` G ) P )
2 trlontrl 
 |-  ( F ( Trails ` G ) P -> F ( ( P ` 0 ) ( TrailsOn ` G ) ( P ` ( # ` F ) ) ) P )
3 1 2 syl 
 |-  ( F ( Paths ` G ) P -> F ( ( P ` 0 ) ( TrailsOn ` G ) ( P ` ( # ` F ) ) ) P )
4 id 
 |-  ( F ( Paths ` G ) P -> F ( Paths ` G ) P )
5 pthiswlk 
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 6 wlkepvtx 
 |-  ( F ( Walks ` G ) P -> ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) )
8 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
9 3simpc 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F e. _V /\ P e. _V ) )
10 8 9 syl 
 |-  ( F ( Walks ` G ) P -> ( F e. _V /\ P e. _V ) )
11 7 10 jca 
 |-  ( F ( Walks ` G ) P -> ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
12 6 ispthson 
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` ( # ` F ) ) ) P <-> ( F ( ( P ` 0 ) ( TrailsOn ` G ) ( P ` ( # ` F ) ) ) P /\ F ( Paths ` G ) P ) ) )
13 5 11 12 3syl 
 |-  ( F ( Paths ` G ) P -> ( F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` ( # ` F ) ) ) P <-> ( F ( ( P ` 0 ) ( TrailsOn ` G ) ( P ` ( # ` F ) ) ) P /\ F ( Paths ` G ) P ) ) )
14 3 4 13 mpbir2and 
 |-  ( F ( Paths ` G ) P -> F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` ( # ` F ) ) ) P )