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 , 𝐴 ⟩ } )