Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wwlk Structured version   Unicode version

Definition df-wwlk 30266
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-wlk 23366. 
w  =  (/) has to be excluded because a walk always consists of at least one vertex, see wlkn0 30232. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
Assertion
Ref Expression
df-wwlk  |- WWalks  =  ( v  e.  _V , 
e  e.  _V  |->  { w  e. Word  v  |  ( w  =/=  (/)  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e ) } )
Distinct variable group:    e, i, v, w

Detailed syntax breakdown of Definition df-wwlk
StepHypRef Expression
1 cwwlk 30264 . 2  class WWalks
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 2967 . . 3  class  _V
5 vw . . . . . . 7  setvar  w
65cv 1368 . . . . . 6  class  w
7 c0 3632 . . . . . 6  class  (/)
86, 7wne 2601 . . . . 5  wff  w  =/=  (/)
9 vi . . . . . . . . . 10  setvar  i
109cv 1368 . . . . . . . . 9  class  i
1110, 6cfv 5413 . . . . . . . 8  class  ( w `
 i )
12 c1 9275 . . . . . . . . . 10  class  1
13 caddc 9277 . . . . . . . . . 10  class  +
1410, 12, 13co 6086 . . . . . . . . 9  class  ( i  +  1 )
1514, 6cfv 5413 . . . . . . . 8  class  ( w `
 ( i  +  1 ) )
1611, 15cpr 3874 . . . . . . 7  class  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }
173cv 1368 . . . . . . . 8  class  e
1817crn 4836 . . . . . . 7  class  ran  e
1916, 18wcel 1756 . . . . . 6  wff  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
20 cc0 9274 . . . . . . 7  class  0
21 chash 12095 . . . . . . . . 9  class  #
226, 21cfv 5413 . . . . . . . 8  class  ( # `  w )
23 cmin 9587 . . . . . . . 8  class  -
2422, 12, 23co 6086 . . . . . . 7  class  ( (
# `  w )  -  1 )
25 cfzo 11540 . . . . . . 7  class ..^
2620, 24, 25co 6086 . . . . . 6  class  ( 0..^ ( ( # `  w
)  -  1 ) )
2719, 9, 26wral 2710 . . . . 5  wff  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
288, 27wa 369 . . . 4  wff  ( w  =/=  (/)  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
)
292cv 1368 . . . . 5  class  v
3029cword 12213 . . . 4  class Word  v
3128, 5, 30crab 2714 . . 3  class  { w  e. Word  v  |  ( w  =/=  (/)  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
) }
322, 3, 4, 4, 31cmpt2 6088 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  { w  e. Word  v  |  ( w  =/=  (/)  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
) } )
331, 32wceq 1369 1  wff WWalks  =  ( v  e.  _V , 
e  e.  _V  |->  { w  e. Word  v  |  ( w  =/=  (/)  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e ) } )
Colors of variables: wff setvar class
This definition is referenced by:  wwlk  30268  wwlkprop  30272
  Copyright terms: Public domain W3C validator