This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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