Theorem eupthi

Description: Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypothesis	eupths.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
Assertion	eupthi	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to \left(F\mathrm{Walks}\left(G\right)P\wedge F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\right)$$

Proof

Step	Hyp	Ref	Expression
1		eupths.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
2	1	iseupthf1o	$$⊢F\mathrm{EulerPaths}\left(G\right)P\leftrightarrow \left(F\mathrm{Walks}\left(G\right)P\wedge F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\right)$$
3	2	biimpi	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to \left(F\mathrm{Walks}\left(G\right)P\wedge F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\right)$$