Theorem eupthistrl

Description: An Eulerian path is a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017) (Revised by AV, 18-Feb-2021)

	Ref	Expression
Assertion	eupthistrl	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Trails}\left(G\right)P$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
2	1	iseupth	$$⊢F\mathrm{EulerPaths}\left(G\right)P\leftrightarrow \left(F\mathrm{Trails}\left(G\right)P\wedge F:\left(0..^\left|F\right|\right)\underset{onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(G\right)\right)$$
3	2	simplbi	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Trails}\left(G\right)P$$