Theorem eupthpf

Description: The P function in an Eulerian path is a function from a finite sequence of nonnegative integers to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

	Ref	Expression
Assertion	eupthpf	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		eupthiswlk	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
2		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
3	2	wlkp	$$⊢F\mathrm{Walks}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)$$
4	1 3	syl	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)$$