Description: Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n1) e(f(n)) p(n) as defined in dfwlks . (Contributed by Alexander van der Vekens, 15Jul2018) (Revised by AV, 8Apr2021)
Ref  Expression  

Assertion  dfwwlksn   WWalksN = ( n e. NN0 , g e. _V > { w e. ( WWalks ` g )  ( # ` w ) = ( n + 1 ) } ) 
Step  Hyp  Ref  Expression 

0  cwwlksn   WWalksN 

1  vn   n 

2  cn0   NN0 

3  vg   g 

4  cvv   _V 

5  vw   w 

6  cwwlks   WWalks 

7  3  cv   g 
8  7 6  cfv   ( WWalks ` g ) 
9  chash   # 

10  5  cv   w 
11  10 9  cfv   ( # ` w ) 
12  1  cv   n 
13  caddc   + 

14  c1   1 

15  12 14 13  co   ( n + 1 ) 
16  11 15  wceq   ( # ` w ) = ( n + 1 ) 
17  16 5 8  crab   { w e. ( WWalks ` g )  ( # ` w ) = ( n + 1 ) } 
18  1 3 2 4 17  cmpo   ( n e. NN0 , g e. _V > { w e. ( WWalks ` g )  ( # ` w ) = ( n + 1 ) } ) 
19  0 18  wceq   WWalksN = ( n e. NN0 , g e. _V > { w e. ( WWalks ` g )  ( # ` w ) = ( n + 1 ) } ) 