This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )