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\mathrm{Paths}\left(G\right)P\to F\mathrm{Trails}\left(G\right)P$$

Proof

Step	Hyp	Ref	Expression
1		ispth	$$⊢F\mathrm{Paths}\left(G\right)P\leftrightarrow \left(F\mathrm{Trails}\left(G\right)P\wedge \mathrm{Fun}{\left({P\upharpoonright }_{\left(1..^\left|F\right|\right)}\right)}^{-1}\wedge P\left[\left\{0,\left|F\right|\right\}\right]\cap P\left[\left(1..^\left|F\right|\right)\right]=\varnothing \right)$$
2	1	simp1bi	$$⊢F\mathrm{Paths}\left(G\right)P\to F\mathrm{Trails}\left(G\right)P$$