Metamath Proof Explorer


Theorem trlontrl

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

Ref Expression
Assertion trlontrl
|- ( F ( Trails ` G ) P -> F ( ( P ` 0 ) ( TrailsOn ` G ) ( P ` ( # ` F ) ) ) P )

Proof

Step Hyp Ref Expression
1 trliswlk
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
2 wlkonwlk
 |-  ( F ( Walks ` G ) P -> F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P )
3 1 2 syl
 |-  ( F ( Trails ` G ) P -> F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P )
4 id
 |-  ( F ( Trails ` G ) P -> F ( Trails ` G ) P )
5 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
6 5 wlkepvtx
 |-  ( F ( Walks ` G ) P -> ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) )
7 wlkv
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
8 3simpc
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F e. _V /\ P e. _V ) )
9 8 anim2i
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) /\ ( G e. _V /\ F e. _V /\ P e. _V ) ) -> ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
10 6 7 9 syl2anc
 |-  ( F ( Walks ` G ) P -> ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
11 1 10 syl
 |-  ( F ( Trails ` G ) P -> ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) )
12 5 istrlson
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( ( P ` 0 ) ( TrailsOn ` G ) ( P ` ( # ` F ) ) ) P <-> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P /\ F ( Trails ` G ) P ) ) )
13 11 12 syl
 |-  ( F ( Trails ` G ) P -> ( F ( ( P ` 0 ) ( TrailsOn ` G ) ( P ` ( # ` F ) ) ) P <-> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P /\ F ( Trails ` G ) P ) ) )
14 3 4 13 mpbir2and
 |-  ( F ( Trails ` G ) P -> F ( ( P ` 0 ) ( TrailsOn ` G ) ( P ` ( # ` F ) ) ) P )