MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wwlk Structured version   Unicode version

Definition df-wwlk 24806
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 24635. 
w  =  (/) has to be excluded because a walk always consists of at least one vertex, see wlkn0 24654. (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 24804 . 2  class WWalks
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 3109 . . 3  class  _V
5 vw . . . . . . 7  setvar  w
65cv 1394 . . . . . 6  class  w
7 c0 3793 . . . . . 6  class  (/)
86, 7wne 2652 . . . . 5  wff  w  =/=  (/)
9 vi . . . . . . . . . 10  setvar  i
109cv 1394 . . . . . . . . 9  class  i
1110, 6cfv 5594 . . . . . . . 8  class  ( w `
 i )
12 c1 9510 . . . . . . . . . 10  class  1
13 caddc 9512 . . . . . . . . . 10  class  +
1410, 12, 13co 6296 . . . . . . . . 9  class  ( i  +  1 )
1514, 6cfv 5594 . . . . . . . 8  class  ( w `
 ( i  +  1 ) )
1611, 15cpr 4034 . . . . . . 7  class  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }
173cv 1394 . . . . . . . 8  class  e
1817crn 5009 . . . . . . 7  class  ran  e
1916, 18wcel 1819 . . . . . 6  wff  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
20 cc0 9509 . . . . . . 7  class  0
21 chash 12408 . . . . . . . . 9  class  #
226, 21cfv 5594 . . . . . . . 8  class  ( # `  w )
23 cmin 9824 . . . . . . . 8  class  -
2422, 12, 23co 6296 . . . . . . 7  class  ( (
# `  w )  -  1 )
25 cfzo 11821 . . . . . . 7  class ..^
2620, 24, 25co 6296 . . . . . 6  class  ( 0..^ ( ( # `  w
)  -  1 ) )
2719, 9, 26wral 2807 . . . . 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 1394 . . . . 5  class  v
3029cword 12538 . . . 4  class Word  v
3128, 5, 30crab 2811 . . 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 6298 . 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 1395 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  24808  wwlkprop  24812
  Copyright terms: Public domain W3C validator