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 ClWWalksN 𝐺 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		clwwlkn	⊢ ( 0 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 0 }
2		rabeq0	⊢ ( { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 0 } = ∅ ↔ ∀ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑤 ) = 0 )
3		0re	⊢ 0 ∈ ℝ
4	3	ltnri	⊢ ¬ 0 < 0
5		breq2	⊢ ( ( ♯ ‘ 𝑤 ) = 0 → ( 0 < ( ♯ ‘ 𝑤 ) ↔ 0 < 0 ) )
6	4 5	mtbiri	⊢ ( ( ♯ ‘ 𝑤 ) = 0 → ¬ 0 < ( ♯ ‘ 𝑤 ) )
7		clwwlkgt0	⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → 0 < ( ♯ ‘ 𝑤 ) )
8	6 7	nsyl3	⊢ ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) → ¬ ( ♯ ‘ 𝑤 ) = 0 )
9	2 8	mprgbir	⊢ { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 0 } = ∅
10	1 9	eqtri	⊢ ( 0 ClWWalksN 𝐺 ) = ∅