This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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