eupths

Description: The Eulerian paths on the graph G . (Contributed by AV, 18-Feb-2021) (Revised by AV, 29-Oct-2021)

		Ref	Expression
	Hypothesis	eupths.i	$⊢ I = iEdg (G)$
	Assertion	eupths	$⊢ EulerPaths (G) = \{⟨f, p⟩ \| (f Trails (G) p \land f : (0 ..^\|f\|) \underset{onto}{⟶} dom I)\}$

Step	Hyp	Ref	Expression
1		eupths.i	$⊢ I = iEdg (G)$
2		fveq2	$⊢ g = G \to iEdg (g) = iEdg (G)$
3	2 1	eqtr4di	$⊢ g = G \to iEdg (g) = I$
4	3	dmeqd	$⊢ g = G \to dom iEdg (g) = dom I$
5		foeq3	$⊢ dom iEdg (g) = dom I \to (f : (0 ..^\|f\|) \underset{onto}{⟶} dom iEdg (g) \leftrightarrow f : (0 ..^\|f\|) \underset{onto}{⟶} dom I)$
6	4 5	syl	$⊢ g = G \to (f : (0 ..^\|f\|) \underset{onto}{⟶} dom iEdg (g) \leftrightarrow f : (0 ..^\|f\|) \underset{onto}{⟶} dom I)$
7		df-eupth	$⊢ EulerPaths = (g \in V ⟼ \{⟨f, p⟩ \| (f Trails (g) p \land f : (0 ..^\|f\|) \underset{onto}{⟶} dom iEdg (g))\})$
8	6 7	fvmptopab	$⊢ EulerPaths (G) = \{⟨f, p⟩ \| (f Trails (G) p \land f : (0 ..^\|f\|) \underset{onto}{⟶} dom I)\}$

Metamath Proof Explorer