Theorem clwwlknon1nloop

Description: If there is no loop at vertex X , the set of (closed) walks on X of length 1 as words over the set of vertices is empty. (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Mar-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	clwwlknon1nloop	$$⊢\left\{X\right\}\notin E\to XC1=\varnothing$$

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	1 2 3	clwwlknon1	$$⊢X\in V\to XC1=\left\{w\in \mathrm{Word}V|\left(w=⟨“X”⟩\wedge \left\{X\right\}\in E\right)\right\}$$
5	4	adantr	$$⊢\left(X\in V\wedge \left\{X\right\}\notin E\right)\to XC1=\left\{w\in \mathrm{Word}V|\left(w=⟨“X”⟩\wedge \left\{X\right\}\in E\right)\right\}$$
6		df-nel	$$⊢\left\{X\right\}\notin E\leftrightarrow \neg \left\{X\right\}\in E$$
7	6	biimpi	$$⊢\left\{X\right\}\notin E\to \neg \left\{X\right\}\in E$$
8	7	olcd	$$⊢\left\{X\right\}\notin E\to \left(\neg w=⟨“X”⟩\vee \neg \left\{X\right\}\in E\right)$$
9	8	ad2antlr	$$⊢\left(\left(X\in V\wedge \left\{X\right\}\notin E\right)\wedge w\in \mathrm{Word}V\right)\to \left(\neg w=⟨“X”⟩\vee \neg \left\{X\right\}\in E\right)$$
10		ianor	$$⊢\neg \left(w=⟨“X”⟩\wedge \left\{X\right\}\in E\right)\leftrightarrow \left(\neg w=⟨“X”⟩\vee \neg \left\{X\right\}\in E\right)$$
11	9 10	sylibr	$$⊢\left(\left(X\in V\wedge \left\{X\right\}\notin E\right)\wedge w\in \mathrm{Word}V\right)\to \neg \left(w=⟨“X”⟩\wedge \left\{X\right\}\in E\right)$$
12	11	ralrimiva	$$⊢\left(X\in V\wedge \left\{X\right\}\notin E\right)\to \forall w\in \mathrm{Word}V\neg \left(w=⟨“X”⟩\wedge \left\{X\right\}\in E\right)$$
13		rabeq0	$$⊢\left\{w\in \mathrm{Word}V|\left(w=⟨“X”⟩\wedge \left\{X\right\}\in E\right)\right\}=\varnothing \leftrightarrow \forall w\in \mathrm{Word}V\neg \left(w=⟨“X”⟩\wedge \left\{X\right\}\in E\right)$$
14	12 13	sylibr	$$⊢\left(X\in V\wedge \left\{X\right\}\notin E\right)\to \left\{w\in \mathrm{Word}V|\left(w=⟨“X”⟩\wedge \left\{X\right\}\in E\right)\right\}=\varnothing$$
15	5 14	eqtrd	$$⊢\left(X\in V\wedge \left\{X\right\}\notin E\right)\to XC1=\varnothing$$
16	2	oveqi	$$⊢XC1=X\mathrm{ClWWalksNOn}\left(G\right)1$$
17	1	eleq2i	$$⊢X\in V\leftrightarrow X\in \mathrm{Vtx}\left(G\right)$$
18	17	notbii	$$⊢\neg X\in V\leftrightarrow \neg X\in \mathrm{Vtx}\left(G\right)$$
19	18	biimpi	$$⊢\neg X\in V\to \neg X\in \mathrm{Vtx}\left(G\right)$$
20	19	intnanrd	$$⊢\neg X\in V\to \neg \left(X\in \mathrm{Vtx}\left(G\right)\wedge 1\in \mathbb{N}\right)$$
21		clwwlknon0	$$⊢\neg \left(X\in \mathrm{Vtx}\left(G\right)\wedge 1\in \mathbb{N}\right)\to X\mathrm{ClWWalksNOn}\left(G\right)1=\varnothing$$
22	20 21	syl	$$⊢\neg X\in V\to X\mathrm{ClWWalksNOn}\left(G\right)1=\varnothing$$
23	16 22	syl5eq	$$⊢\neg X\in V\to XC1=\varnothing$$
24	23	adantr	$$⊢\left(\neg X\in V\wedge \left\{X\right\}\notin E\right)\to XC1=\varnothing$$
25	15 24	pm2.61ian	$$⊢\left\{X\right\}\notin E\to XC1=\varnothing$$