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

Metamath Proof Explorer

Theorem iswwlksn

Description: A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion iswwlksn 
|- ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 wwlksn 
 |-  ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
2 1 eleq2d 
 |-  ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> W e. { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) )
3 fveqeq2 
 |-  ( w = W -> ( ( # ` w ) = ( N + 1 ) <-> ( # ` W ) = ( N + 1 ) ) )
4 3 elrab 
 |-  ( W e. { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
5 2 4 bitrdi 
 |-  ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )