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 𝐼 = ( iEdg ‘ 𝐺 )
Assertion eupthfi ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → dom 𝐼 ∈ Fin )

Proof

Step Hyp Ref Expression
1 eupths.i 𝐼 = ( iEdg ‘ 𝐺 )
2 fzofi ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ Fin
3 1 eupthf1o ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 )
4 ovex ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V
5 4 f1oen ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ≈ dom 𝐼 )
6 ensym ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ≈ dom 𝐼 → dom 𝐼 ≈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
7 3 5 6 3syl ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → dom 𝐼 ≈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
8 enfii ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ Fin ∧ dom 𝐼 ≈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → dom 𝐼 ∈ Fin )
9 2 7 8 sylancr ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → dom 𝐼 ∈ Fin )