Metamath Proof Explorer

Theorem eupthfi

Description: Any graph with an Eulerian path is of finite size, i.e. with a finite number of edges. (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 18-Feb-2021)

		Ref	Expression
	Hypothesis	eupths.i	$⊢ I = iEdg (G)$
	Assertion	eupthfi	$⊢ F EulerPaths (G) P \to dom I \in Fin$

Proof

Step	Hyp	Ref	Expression
1		eupths.i	$⊢ I = iEdg (G)$
2		fzofi	$⊢ (0 ..^\|F\|) \in Fin$
3	1	eupthf1o	$⊢ F EulerPaths (G) P \to F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I$
4		ovex	$⊢ (0 ..^\|F\|) \in V$
5	4	f1oen	$⊢ F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \to (0 ..^\|F\|) \approx dom I$
6		ensym	$⊢ (0 ..^\|F\|) \approx dom I \to dom I \approx (0 ..^\|F\|)$
7	3 5 6	3syl	$⊢ F EulerPaths (G) P \to dom I \approx (0 ..^\|F\|)$
8		enfii	$⊢ ((0 ..^\|F\|) \in Fin \land dom I \approx (0 ..^\|F\|)) \to dom I \in Fin$
9	2 7 8	sylancr	$⊢ F EulerPaths (G) P \to dom I \in Fin$