Theorem wwlksnon

Description: 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, 11-May-2021)

	Ref	Expression
Hypothesis	wwlksnon.v	|- V = ( Vtx ` G )
Assertion	wwlksnon	|- ( ( N e. NN0 /\ G e. U ) -> ( N WWalksNOn G ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) )

Proof

Step	Hyp	Ref	Expression
1		wwlksnon.v	|- V = ( Vtx ` G )
2		df-wwlksnon	|- WWalksNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) )
3	2	a1i	|- ( ( N e. NN0 /\ G e. U ) -> WWalksNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) ) )
4		fveq2	|- ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
5	4 1	eqtr4di	|- ( g = G -> ( Vtx ` g ) = V )
6	5	adantl	|- ( ( n = N /\ g = G ) -> ( Vtx ` g ) = V )
7		oveq12	|- ( ( n = N /\ g = G ) -> ( n WWalksN g ) = ( N WWalksN G ) )
8		fveqeq2	|- ( n = N -> ( ( w ` n ) = b <-> ( w ` N ) = b ) )
9	8	anbi2d	|- ( n = N -> ( ( ( w ` 0 ) = a /\ ( w ` n ) = b ) <-> ( ( w ` 0 ) = a /\ ( w ` N ) = b ) ) )
10	9	adantr	|- ( ( n = N /\ g = G ) -> ( ( ( w ` 0 ) = a /\ ( w ` n ) = b ) <-> ( ( w ` 0 ) = a /\ ( w ` N ) = b ) ) )
11	7 10	rabeqbidv	|- ( ( n = N /\ g = G ) -> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } )
12	6 6 11	mpoeq123dv	|- ( ( n = N /\ g = G ) -> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) )
13	12	adantl	|- ( ( ( N e. NN0 /\ G e. U ) /\ ( n = N /\ g = G ) ) -> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) )
14		simpl	|- ( ( N e. NN0 /\ G e. U ) -> N e. NN0 )
15		elex	|- ( G e. U -> G e. _V )
16	15	adantl	|- ( ( N e. NN0 /\ G e. U ) -> G e. _V )
17	1	fvexi	|- V e. _V
18	17 17	mpoex	|- ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) e. _V
19	18	a1i	|- ( ( N e. NN0 /\ G e. U ) -> ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) e. _V )
20	3 13 14 16 19	ovmpod	|- ( ( N e. NN0 /\ G e. U ) -> ( N WWalksNOn G ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) )