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 )