Metamath Proof Explorer


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 syl6bi
 |-  ( ( 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 ) )