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