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 G ) = (/)

Proof

Step Hyp Ref Expression
1 clwwlkn 
 |-  ( 0 ClWWalksN G ) = { w e. ( ClWWalks ` G ) | ( # ` w ) = 0 }
2 rabeq0 
 |-  ( { w e. ( ClWWalks ` G ) | ( # ` w ) = 0 } = (/) <-> A. w e. ( ClWWalks ` G ) -. ( # ` w ) = 0 )
3 0re 
 |-  0 e. RR
4 3 ltnri 
 |-  -. 0 < 0
5 breq2 
 |-  ( ( # ` w ) = 0 -> ( 0 < ( # ` w ) <-> 0 < 0 ) )
6 4 5 mtbiri 
 |-  ( ( # ` w ) = 0 -> -. 0 < ( # ` w ) )
7 clwwlkgt0 
 |-  ( w e. ( ClWWalks ` G ) -> 0 < ( # ` w ) )
8 6 7 nsyl3 
 |-  ( w e. ( ClWWalks ` G ) -> -. ( # ` w ) = 0 )
9 2 8 mprgbir 
 |-  { w e. ( ClWWalks ` G ) | ( # ` w ) = 0 } = (/)
10 1 9 eqtri 
 |-  ( 0 ClWWalksN G ) = (/)