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

Metamath Proof Explorer

Theorem trliswlk

Description: A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 7-Jan-2021) (Proof shortened by AV, 29-Oct-2021)

		Ref	Expression
	Assertion	trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$

Proof

Step	Hyp	Ref	Expression
1		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
2	1	simplbi	$⊢ F Trails (G) P \to F Walks (G) P$