Theorem wwlkbp

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

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

Proof

Step	Hyp	Ref	Expression
1		wwlkbp.v	|- V = ( Vtx ` G )
2		elfvex	|- ( W e. ( WWalks ` G ) -> G e. _V )
3		eqid	|- ( Edg ` G ) = ( Edg ` G )
4	1 3	iswwlks	|- ( W e. ( WWalks ` G ) <-> ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
5	4	simp2bi	|- ( W e. ( WWalks ` G ) -> W e. Word V )
6	2 5	jca	|- ( W e. ( WWalks ` G ) -> ( G e. _V /\ W e. Word V ) )