Theorem is0wlk

Description: A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypothesis	0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	is0wlk	$$⊢\left(P=\left\{⟨0,N⟩\right\}\wedge N\in V\right)\to \varnothing \mathrm{Walks}\left(G\right)P$$

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		1fv	$$⊢\left(N\in V\wedge P=\left\{⟨0,N⟩\right\}\right)\to \left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)$$
3	2	ancoms	$$⊢\left(P=\left\{⟨0,N⟩\right\}\wedge N\in V\right)\to \left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)$$
4	3	simpld	$$⊢\left(P=\left\{⟨0,N⟩\right\}\wedge N\in V\right)\to P:\left(0\dots 0\right)⟶V$$
5	1	1vgrex	$$⊢N\in V\to G\in \mathrm{V}$$
6	5	adantl	$$⊢\left(P=\left\{⟨0,N⟩\right\}\wedge N\in V\right)\to G\in \mathrm{V}$$
7	1	0wlk	$$⊢G\in \mathrm{V}\to \left(\varnothing \mathrm{Walks}\left(G\right)P\leftrightarrow P:\left(0\dots 0\right)⟶V\right)$$
8	6 7	syl	$$⊢\left(P=\left\{⟨0,N⟩\right\}\wedge N\in V\right)\to \left(\varnothing \mathrm{Walks}\left(G\right)P\leftrightarrow P:\left(0\dots 0\right)⟶V\right)$$
9	4 8	mpbird	$$⊢\left(P=\left\{⟨0,N⟩\right\}\wedge N\in V\right)\to \varnothing \mathrm{Walks}\left(G\right)P$$