Metamath Proof Explorer


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 0 G U N WWalksNOn G = a V , b V w 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 0 , g V a Vtx g , b Vtx g w n WWalksN g | w 0 = a w n = b
3 2 a1i N 0 G U WWalksNOn = n 0 , g V a Vtx g , b Vtx g w 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 n WWalksN g | w 0 = a w n = b = w N WWalksN G | w 0 = a w N = b
12 6 6 11 mpoeq123dv n = N g = G a Vtx g , b Vtx g w n WWalksN g | w 0 = a w n = b = a V , b V w N WWalksN G | w 0 = a w N = b
13 12 adantl N 0 G U n = N g = G a Vtx g , b Vtx g w n WWalksN g | w 0 = a w n = b = a V , b V w N WWalksN G | w 0 = a w N = b
14 simpl N 0 G U N 0
15 elex G U G V
16 15 adantl N 0 G U G V
17 1 fvexi V V
18 17 17 mpoex a V , b V w N WWalksN G | w 0 = a w N = b V
19 18 a1i N 0 G U a V , b V w N WWalksN G | w 0 = a w N = b V
20 3 13 14 16 19 ovmpod N 0 G U N WWalksNOn G = a V , b V w N WWalksN G | w 0 = a w N = b