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

Metamath Proof Explorer

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 EulerPaths (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$

Proof

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