Theorem wlkn0

Description: The sequence of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018) (Revised by AV, 2-Jan-2021)

	Ref	Expression
Assertion	wlkn0	$$⊢F\mathrm{Walks}\left(G\right)P\to P\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
2	1	wlkp	$$⊢F\mathrm{Walks}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)$$
3		fdm	$$⊢P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)\to \mathrm{dom}P=\left(0\dots \left|F\right|\right)$$
4	3	eqcomd	$$⊢P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)\to \left(0\dots \left|F\right|\right)=\mathrm{dom}P$$
5	2 4	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(0\dots \left|F\right|\right)=\mathrm{dom}P$$
6		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
7		elnn0uz	$$⊢\left|F\right|\in {\mathbb{N}}_0\leftrightarrow \left|F\right|\in {\mathbb{Z}}_{\ge 0}$$
8		fzn0	$$⊢\left(0\dots \left|F\right|\right)\ne \varnothing \leftrightarrow \left|F\right|\in {\mathbb{Z}}_{\ge 0}$$
9	7 8	sylbb2	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \left(0\dots \left|F\right|\right)\ne \varnothing$$
10	6 9	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(0\dots \left|F\right|\right)\ne \varnothing$$
11	5 10	eqnetrrd	$$⊢F\mathrm{Walks}\left(G\right)P\to \mathrm{dom}P\ne \varnothing$$
12		frel	$$⊢P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)\to \mathrm{Rel}P$$
13	2 12	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to \mathrm{Rel}P$$
14		reldm0	$$⊢\mathrm{Rel}P\to \left(P=\varnothing \leftrightarrow \mathrm{dom}P=\varnothing \right)$$
15	14	necon3bid	$$⊢\mathrm{Rel}P\to \left(P\ne \varnothing \leftrightarrow \mathrm{dom}P\ne \varnothing \right)$$
16	13 15	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(P\ne \varnothing \leftrightarrow \mathrm{dom}P\ne \varnothing \right)$$
17	11 16	mpbird	$$⊢F\mathrm{Walks}\left(G\right)P\to P\ne \varnothing$$