Theorem clwwlkn0

Description: There is no closed walk of length 0 (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 24-Apr-2021)

	Ref	Expression
Assertion	clwwlkn0	$$⊢0\mathrm{ClWWalksN}G=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		clwwlkn	$$⊢0\mathrm{ClWWalksN}G=\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=0\right\}$$
2		rabeq0	$$⊢\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=0\right\}=\varnothing \leftrightarrow \forall w\in \mathrm{ClWWalks}\left(G\right)\neg \left|w\right|=0$$
3		0re	$$⊢0\in ℝ$$
4	3	ltnri	$$⊢\neg 0<0$$
5		breq2	$$⊢\left|w\right|=0\to \left(0<\left|w\right|\leftrightarrow 0<0\right)$$
6	4 5	mtbiri	$$⊢\left|w\right|=0\to \neg 0<\left|w\right|$$
7		clwwlkgt0	$$⊢w\in \mathrm{ClWWalks}\left(G\right)\to 0<\left|w\right|$$
8	6 7	nsyl3	$$⊢w\in \mathrm{ClWWalks}\left(G\right)\to \neg \left|w\right|=0$$
9	2 8	mprgbir	$$⊢\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=0\right\}=\varnothing$$
10	1 9	eqtri	$$⊢0\mathrm{ClWWalksN}G=\varnothing$$