Theorem clwwlk0on0

Description: There is no word over the set of vertices representing a closed walk on vertex X of length 0 in a graph G . (Contributed by AV, 17-Feb-2022) (Revised by AV, 25-Feb-2022)

	Ref	Expression
Assertion	clwwlk0on0	$$⊢X\mathrm{ClWWalksNOn}\left(G\right)0=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$$⊢v=X\to \left(w\left(0\right)=v\leftrightarrow w\left(0\right)=X\right)$$
2	1	rabbidv	$$⊢v=X\to \left\{w\in \left(n\mathrm{ClWWalksN}G\right)|w\left(0\right)=v\right\}=\left\{w\in \left(n\mathrm{ClWWalksN}G\right)|w\left(0\right)=X\right\}$$
3		oveq1	$$⊢n=0\to n\mathrm{ClWWalksN}G=0\mathrm{ClWWalksN}G$$
4		clwwlkn0	$$⊢0\mathrm{ClWWalksN}G=\varnothing$$
5	3 4	eqtrdi	$$⊢n=0\to n\mathrm{ClWWalksN}G=\varnothing$$
6	5	rabeqdv	$$⊢n=0\to \left\{w\in \left(n\mathrm{ClWWalksN}G\right)|w\left(0\right)=X\right\}=\left\{w\in \varnothing |w\left(0\right)=X\right\}$$
7		clwwlknonmpo	$$⊢\mathrm{ClWWalksNOn}\left(G\right)=\left(v\in \mathrm{Vtx}\left(G\right),n\in {\mathbb{N}}_0⟼\left\{w\in \left(n\mathrm{ClWWalksN}G\right)|w\left(0\right)=v\right\}\right)$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9	8	rabex	$$⊢\left\{w\in \varnothing |w\left(0\right)=X\right\}\in \mathrm{V}$$
10	2 6 7 9	ovmpo	$$⊢\left(X\in \mathrm{Vtx}\left(G\right)\wedge 0\in {\mathbb{N}}_0\right)\to X\mathrm{ClWWalksNOn}\left(G\right)0=\left\{w\in \varnothing |w\left(0\right)=X\right\}$$
11		rab0	$$⊢\left\{w\in \varnothing |w\left(0\right)=X\right\}=\varnothing$$
12	10 11	eqtrdi	$$⊢\left(X\in \mathrm{Vtx}\left(G\right)\wedge 0\in {\mathbb{N}}_0\right)\to X\mathrm{ClWWalksNOn}\left(G\right)0=\varnothing$$
13	7	mpondm0	$$⊢\neg \left(X\in \mathrm{Vtx}\left(G\right)\wedge 0\in {\mathbb{N}}_0\right)\to X\mathrm{ClWWalksNOn}\left(G\right)0=\varnothing$$
14	12 13	pm2.61i	$$⊢X\mathrm{ClWWalksNOn}\left(G\right)0=\varnothing$$