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 ClWWalksN G = \emptyset$

Proof

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

Metamath Proof Explorer

Theorem clwwlkn0

Proof