Metamath Proof Explorer

Theorem upgreupthi

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

		Ref	Expression
	Hypotheses	eupths.i	$⊢ I = iEdg (G)$
		upgriseupth.v	$⊢ V = Vtx (G)$
	Assertion	upgreupthi	$⊢ (G \in UPGraph \land F EulerPaths (G) P) \to (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$

Proof

Step	Hyp	Ref	Expression
1		eupths.i	$⊢ I = iEdg (G)$
2		upgriseupth.v	$⊢ V = Vtx (G)$
3	1 2	upgriseupth	$⊢ G \in UPGraph \to (F EulerPaths (G) P \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
4	3	biimpa	$⊢ (G \in UPGraph \land F EulerPaths (G) P) \to (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$