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