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=\mathrm{iEdg}\left(G\right)$$
Assertion	eupthfi	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to \mathrm{dom}I\in \mathrm{Fin}$$

Proof

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