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

Metamath Proof Explorer

Theorem pthistrl

Description: A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Assertion	pthistrl	$⊢ F Paths (G) P \to F Trails (G) P$

Proof

Step	Hyp	Ref	Expression
1		ispth	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
2	1	simp1bi	$⊢ F Paths (G) P \to F Trails (G) P$