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