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 ⊢ V = Vtx ⁡ G
eupth0.i ⊢ I = iEdg ⁡ G
Assertion eupth0 ⊢ A ∈ V ∧ I = ∅ → ∅ EulerPaths ⁡ G 0 A

Proof

Step Hyp Ref Expression
1 eupth0.v ⊢ V = Vtx ⁡ G
2 eupth0.i ⊢ I = iEdg ⁡ G
3 eqidd ⊢ A ∈ V → 0 A = 0 A
4 1 is0wlk ⊢ 0 A = 0 A ∧ A ∈ V → ∅ Walks ⁡ G 0 A
5 3 4 mpancom ⊢ A ∈ V → ∅ Walks ⁡ G 0 A
6 f1o0 ⊢ ∅ : ∅ ⟶ 1-1 onto ∅
7 eqidd ⊢ I = ∅ → ∅ = ∅
8 hash0 ⊢ ∅ = 0
9 8 oveq2i ⊢ 0 ..^ ∅ = 0 ..^ 0
10 fzo0 ⊢ 0 ..^ 0 = ∅
11 9 10 eqtri ⊢ 0 ..^ ∅ = ∅
12 11 a1i ⊢ I = ∅ → 0 ..^ ∅ = ∅
13 dmeq ⊢ I = ∅ → dom ⁡ I = dom ⁡ ∅
14 dm0 ⊢ dom ⁡ ∅ = ∅
15 13 14 eqtrdi ⊢ I = ∅ → dom ⁡ I = ∅
16 7 12 15 f1oeq123d ⊢ I = ∅ → ∅ : 0 ..^ ∅ ⟶ 1-1 onto dom ⁡ I ↔ ∅ : ∅ ⟶ 1-1 onto ∅
17 6 16 mpbiri ⊢ I = ∅ → ∅ : 0 ..^ ∅ ⟶ 1-1 onto dom ⁡ I
18 5 17 anim12i ⊢ A ∈ V ∧ I = ∅ → ∅ Walks ⁡ G 0 A ∧ ∅ : 0 ..^ ∅ ⟶ 1-1 onto dom ⁡ I
19 2 iseupthf1o ⊢ ∅ EulerPaths ⁡ G 0 A ↔ ∅ Walks ⁡ G 0 A ∧ ∅ : 0 ..^ ∅ ⟶ 1-1 onto dom ⁡ I
20 18 19 sylibr ⊢ A ∈ V ∧ I = ∅ → ∅ EulerPaths ⁡ G 0 A