Metamath Proof Explorer

Definition df-wwlks

Description: Define the set of all walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks . w = (/) has to be excluded because a walk always consists of at least one vertex, see wlkn0 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion df-wwlks 
|- WWalks = ( g e. _V |-> { w e. Word ( Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlks 
 |-  WWalks
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vw 
 |-  w
4 cvtx 
 |-  Vtx
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( Vtx ` g )
7 6 cword 
 |-  Word ( Vtx ` g )
8 3 cv 
 |-  w
9 c0 
 |-  (/)
10 8 9 wne 
 |-  w =/= (/)
11 vi 
 |-  i
12 cc0 
 |-  0
13 cfzo 
 |-  ..^
14 chash 
 |-  #
15 8 14 cfv 
 |-  ( # ` w )
16 cmin 
 |-  -
17 c1 
 |-  1
18 15 17 16 co 
 |-  ( ( # ` w ) - 1 )
19 12 18 13 co 
 |-  ( 0 ..^ ( ( # ` w ) - 1 ) )
20 11 cv 
 |-  i
21 20 8 cfv 
 |-  ( w ` i )
22 caddc 
 |-  +
23 20 17 22 co 
 |-  ( i + 1 )
24 23 8 cfv 
 |-  ( w ` ( i + 1 ) )
25 21 24 cpr 
 |-  { ( w ` i ) , ( w ` ( i + 1 ) ) }
26 cedg 
 |-  Edg
27 5 26 cfv 
 |-  ( Edg ` g )
28 25 27 wcel 
 |-  { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g )
29 28 11 19 wral 
 |-  A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g )
30 10 29 wa 
 |-  ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) )
31 30 3 7 crab 
 |-  { w e. Word ( Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) ) }
32 1 2 31 cmpt 
 |-  ( g e. _V |-> { w e. Word ( Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) ) } )
33 0 32 wceq 
 |-  WWalks = ( g e. _V |-> { w e. Word ( Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) ) } )