Theorem wwlkswwlksn

Description: A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018) (Revised by AV, 12-Apr-2021)

	Ref	Expression
Assertion	wwlkswwlksn	|- ( W e. ( N WWalksN G ) -> W e. ( WWalks ` G ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
2	1	wwlknbp	|- ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word ( Vtx ` G ) ) )
3		iswwlksn	|- ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
4	3	3ad2ant2	|- ( ( G e. _V /\ N e. NN0 /\ W e. Word ( Vtx ` G ) ) -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
5		simpl	|- ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> W e. ( WWalks ` G ) )
6	4 5	biimtrdi	|- ( ( G e. _V /\ N e. NN0 /\ W e. Word ( Vtx ` G ) ) -> ( W e. ( N WWalksN G ) -> W e. ( WWalks ` G ) ) )
7	2 6	mpcom	|- ( W e. ( N WWalksN G ) -> W e. ( WWalks ` G ) )