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=\mathrm{Vtx}\left(G\right)$$
	eupth0.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
Assertion	eupth0	$$⊢\left(A\in V\wedge I=\varnothing \right)\to \varnothing \mathrm{EulerPaths}\left(G\right)\left\{⟨0,A⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eupth0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eupth0.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		eqidd	$$⊢A\in V\to \left\{⟨0,A⟩\right\}=\left\{⟨0,A⟩\right\}$$
4	1	is0wlk	$$⊢\left(\left\{⟨0,A⟩\right\}=\left\{⟨0,A⟩\right\}\wedge A\in V\right)\to \varnothing \mathrm{Walks}\left(G\right)\left\{⟨0,A⟩\right\}$$
5	3 4	mpancom	$$⊢A\in V\to \varnothing \mathrm{Walks}\left(G\right)\left\{⟨0,A⟩\right\}$$
6		f1o0	$$⊢\varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing$$
7		eqidd	$$⊢I=\varnothing \to \varnothing =\varnothing$$
8		hash0	$$⊢\left|\varnothing \right|=0$$
9	8	oveq2i	$$⊢\left(0..^\left|\varnothing \right|\right)=\left(0..^0\right)$$
10		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
11	9 10	eqtri	$$⊢\left(0..^\left|\varnothing \right|\right)=\varnothing$$
12	11	a1i	$$⊢I=\varnothing \to \left(0..^\left|\varnothing \right|\right)=\varnothing$$
13		dmeq	$$⊢I=\varnothing \to \mathrm{dom}I=\mathrm{dom}\varnothing$$
14		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
15	13 14	eqtrdi	$$⊢I=\varnothing \to \mathrm{dom}I=\varnothing$$
16	7 12 15	f1oeq123d	$$⊢I=\varnothing \to \left(\varnothing :\left(0..^\left|\varnothing \right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\leftrightarrow \varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing \right)$$
17	6 16	mpbiri	$$⊢I=\varnothing \to \varnothing :\left(0..^\left|\varnothing \right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I$$
18	5 17	anim12i	$$⊢\left(A\in V\wedge I=\varnothing \right)\to \left(\varnothing \mathrm{Walks}\left(G\right)\left\{⟨0,A⟩\right\}\wedge \varnothing :\left(0..^\left|\varnothing \right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\right)$$
19	2	iseupthf1o	$$⊢\varnothing \mathrm{EulerPaths}\left(G\right)\left\{⟨0,A⟩\right\}\leftrightarrow \left(\varnothing \mathrm{Walks}\left(G\right)\left\{⟨0,A⟩\right\}\wedge \varnothing :\left(0..^\left|\varnothing \right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}I\right)$$
20	18 19	sylibr	$$⊢\left(A\in V\wedge I=\varnothing \right)\to \varnothing \mathrm{EulerPaths}\left(G\right)\left\{⟨0,A⟩\right\}$$