Theorem clwwlkbp

Description: Basic properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 24-Apr-2021)

	Ref	Expression
Hypothesis	clwwlkbp.v	|- V = ( Vtx ` G )
Assertion	clwwlkbp	|- ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlkbp.v	|- V = ( Vtx ` G )
2		elfvex	|- ( W e. ( ClWWalks ` G ) -> G e. _V )
3		eqid	|- ( Edg ` G ) = ( Edg ` G )
4	1 3	isclwwlk	|- ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
5	4	simp1bi	|- ( W e. ( ClWWalks ` G ) -> ( W e. Word V /\ W =/= (/) ) )
6		3anass	|- ( ( G e. _V /\ W e. Word V /\ W =/= (/) ) <-> ( G e. _V /\ ( W e. Word V /\ W =/= (/) ) ) )
7	2 5 6	sylanbrc	|- ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) )