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

Metamath Proof Explorer

Theorem wwlknon

Description: An element of the set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Assertion wwlknon 
|- ( W e. ( A ( N WWalksNOn G ) B ) <-> ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = A /\ ( W ` N ) = B ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( w = W -> ( w ` 0 ) = ( W ` 0 ) )
2 1 eqeq1d 
 |-  ( w = W -> ( ( w ` 0 ) = A <-> ( W ` 0 ) = A ) )
3 fveq1 
 |-  ( w = W -> ( w ` N ) = ( W ` N ) )
4 3 eqeq1d 
 |-  ( w = W -> ( ( w ` N ) = B <-> ( W ` N ) = B ) )
5 2 4 anbi12d 
 |-  ( w = W -> ( ( ( w ` 0 ) = A /\ ( w ` N ) = B ) <-> ( ( W ` 0 ) = A /\ ( W ` N ) = B ) ) )
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 6 iswwlksnon 
 |-  ( A ( N WWalksNOn G ) B ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) }
8 5 7 elrab2 
 |-  ( W e. ( A ( N WWalksNOn G ) B ) <-> ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = A /\ ( W ` N ) = B ) ) )
9 3anass 
 |-  ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = A /\ ( W ` N ) = B ) <-> ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = A /\ ( W ` N ) = B ) ) )
10 8 9 bitr4i 
 |-  ( W e. ( A ( N WWalksNOn G ) B ) <-> ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = A /\ ( W ` N ) = B ) )