Theorem 0wlkons1

Description: A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021)

	Ref	Expression
Hypothesis	0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	0wlkons1	$$⊢N\in V\to \varnothing \left(N\mathrm{WalksOn}\left(G\right)N\right)⟨“N”⟩$$

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		s1val	$$⊢N\in V\to ⟨“N”⟩=\left\{⟨0,N⟩\right\}$$
3		0z	$$⊢0\in \mathbb{Z}$$
4	3	jctl	$$⊢N\in V\to \left(0\in \mathbb{Z}\wedge N\in V\right)$$
5		f1sng	$$⊢\left(0\in \mathbb{Z}\wedge N\in V\right)\to \left\{⟨0,N⟩\right\}:\left\{0\right\}\underset{1-1}{⟶}V$$
6		f1f	$$⊢\left\{⟨0,N⟩\right\}:\left\{0\right\}\underset{1-1}{⟶}V\to \left\{⟨0,N⟩\right\}:\left\{0\right\}⟶V$$
7	4 5 6	3syl	$$⊢N\in V\to \left\{⟨0,N⟩\right\}:\left\{0\right\}⟶V$$
8		id	$$⊢⟨“N”⟩=\left\{⟨0,N⟩\right\}\to ⟨“N”⟩=\left\{⟨0,N⟩\right\}$$
9		fzsn	$$⊢0\in \mathbb{Z}\to \left(0\dots 0\right)=\left\{0\right\}$$
10	3 9	mp1i	$$⊢⟨“N”⟩=\left\{⟨0,N⟩\right\}\to \left(0\dots 0\right)=\left\{0\right\}$$
11	8 10	feq12d	$$⊢⟨“N”⟩=\left\{⟨0,N⟩\right\}\to \left(⟨“N”⟩:\left(0\dots 0\right)⟶V\leftrightarrow \left\{⟨0,N⟩\right\}:\left\{0\right\}⟶V\right)$$
12	7 11	syl5ibrcom	$$⊢N\in V\to \left(⟨“N”⟩=\left\{⟨0,N⟩\right\}\to ⟨“N”⟩:\left(0\dots 0\right)⟶V\right)$$
13	2 12	mpd	$$⊢N\in V\to ⟨“N”⟩:\left(0\dots 0\right)⟶V$$
14		s1fv	$$⊢N\in V\to ⟨“N”⟩\left(0\right)=N$$
15	1	0wlkon	$$⊢\left(⟨“N”⟩:\left(0\dots 0\right)⟶V\wedge ⟨“N”⟩\left(0\right)=N\right)\to \varnothing \left(N\mathrm{WalksOn}\left(G\right)N\right)⟨“N”⟩$$
16	13 14 15	syl2anc	$$⊢N\in V\to \varnothing \left(N\mathrm{WalksOn}\left(G\right)N\right)⟨“N”⟩$$