This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eupth0

Description: There is an Eulerian path on an empty graph, i.e. a graph with at least one vertex, but without an edge. (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 5-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypotheses eupth0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
eupth0.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion eupth0 ( ( 𝐴 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ∅ ( EulerPaths ‘ 𝐺 ) { ⟨ 0 , 𝐴 ⟩ } )

Proof

Step Hyp Ref Expression
1 eupth0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eupth0.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 eqidd ⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 0 , 𝐴 ⟩ } = { ⟨ 0 , 𝐴 ⟩ } )
4 1 is0wlk ⊢ ( ( { ⟨ 0 , 𝐴 ⟩ } = { ⟨ 0 , 𝐴 ⟩ } ∧ 𝐴 ∈ 𝑉 ) → ∅ ( Walks ‘ 𝐺 ) { ⟨ 0 , 𝐴 ⟩ } )
5 3 4 mpancom ⊢ ( 𝐴 ∈ 𝑉 → ∅ ( Walks ‘ 𝐺 ) { ⟨ 0 , 𝐴 ⟩ } )
6 f1o0 ⊢ ∅ : ∅ –1-1-onto→ ∅
7 eqidd ⊢ ( 𝐼 = ∅ → ∅ = ∅ )
8 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
9 8 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ∅ ) ) = ( 0 ..^ 0 )
10 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
11 9 10 eqtri ⊢ ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅
12 11 a1i ⊢ ( 𝐼 = ∅ → ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅ )
13 dmeq ⊢ ( 𝐼 = ∅ → dom 𝐼 = dom ∅ )
14 dm0 ⊢ dom ∅ = ∅
15 13 14 eqtrdi ⊢ ( 𝐼 = ∅ → dom 𝐼 = ∅ )
16 7 12 15 f1oeq123d ⊢ ( 𝐼 = ∅ → ( ∅ : ( 0 ..^ ( ♯ ‘ ∅ ) ) –1-1-onto→ dom 𝐼 ↔ ∅ : ∅ –1-1-onto→ ∅ ) )
17 6 16 mpbiri ⊢ ( 𝐼 = ∅ → ∅ : ( 0 ..^ ( ♯ ‘ ∅ ) ) –1-1-onto→ dom 𝐼 )
18 5 17 anim12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ( ∅ ( Walks ‘ 𝐺 ) { ⟨ 0 , 𝐴 ⟩ } ∧ ∅ : ( 0 ..^ ( ♯ ‘ ∅ ) ) –1-1-onto→ dom 𝐼 ) )
19 2 iseupthf1o ⊢ ( ∅ ( EulerPaths ‘ 𝐺 ) { ⟨ 0 , 𝐴 ⟩ } ↔ ( ∅ ( Walks ‘ 𝐺 ) { ⟨ 0 , 𝐴 ⟩ } ∧ ∅ : ( 0 ..^ ( ♯ ‘ ∅ ) ) –1-1-onto→ dom 𝐼 ) )
20 18 19 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ∅ ( EulerPaths ‘ 𝐺 ) { ⟨ 0 , 𝐴 ⟩ } )