Theorem clwwlknon1sn

Description: The set of (closed) walks on vertex X of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of X iff there is a loop at X . (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Feb-2022)

	Ref	Expression
Hypotheses	clwwlknon1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	clwwlknon1.c	$$⊢C=\mathrm{ClWWalksNOn}\left(G\right)$$
	clwwlknon1.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	clwwlknon1sn	$$⊢X\in V\to \left(XC1=\left\{⟨“X”⟩\right\}\leftrightarrow \left\{X\right\}\in E\right)$$

Proof

Step	Hyp	Ref	Expression
1		clwwlknon1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		clwwlknon1.c	$$⊢C=\mathrm{ClWWalksNOn}\left(G\right)$$
3		clwwlknon1.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
4		df-nel	$$⊢\left\{X\right\}\notin E\leftrightarrow \neg \left\{X\right\}\in E$$
5	1 2 3	clwwlknon1nloop	$$⊢\left\{X\right\}\notin E\to XC1=\varnothing$$
6	5	adantl	$$⊢\left(X\in V\wedge \left\{X\right\}\notin E\right)\to XC1=\varnothing$$
7		s1cli	$$⊢⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
8	7	elexi	$$⊢⟨“X”⟩\in \mathrm{V}$$
9	8	snnz	$$⊢\left\{⟨“X”⟩\right\}\ne \varnothing$$
10	9	nesymi	$$⊢\neg \varnothing =\left\{⟨“X”⟩\right\}$$
11		eqeq1	$$⊢XC1=\varnothing \to \left(XC1=\left\{⟨“X”⟩\right\}\leftrightarrow \varnothing =\left\{⟨“X”⟩\right\}\right)$$
12	10 11	mtbiri	$$⊢XC1=\varnothing \to \neg XC1=\left\{⟨“X”⟩\right\}$$
13	6 12	syl	$$⊢\left(X\in V\wedge \left\{X\right\}\notin E\right)\to \neg XC1=\left\{⟨“X”⟩\right\}$$
14	13	ex	$$⊢X\in V\to \left(\left\{X\right\}\notin E\to \neg XC1=\left\{⟨“X”⟩\right\}\right)$$
15	4 14	biimtrrid	$$⊢X\in V\to \left(\neg \left\{X\right\}\in E\to \neg XC1=\left\{⟨“X”⟩\right\}\right)$$
16	15	con4d	$$⊢X\in V\to \left(XC1=\left\{⟨“X”⟩\right\}\to \left\{X\right\}\in E\right)$$
17	1 2 3	clwwlknon1loop	$$⊢\left(X\in V\wedge \left\{X\right\}\in E\right)\to XC1=\left\{⟨“X”⟩\right\}$$
18	17	ex	$$⊢X\in V\to \left(\left\{X\right\}\in E\to XC1=\left\{⟨“X”⟩\right\}\right)$$
19	16 18	impbid	$$⊢X\in V\to \left(XC1=\left\{⟨“X”⟩\right\}\leftrightarrow \left\{X\right\}\in E\right)$$