Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wwlks Structured version   Visualization version   GIF version

Definition df-wwlks 41033
 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-1wlks 40800. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 26055. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
Assertion
Ref Expression
df-wwlks WWalkS = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
Distinct variable group:   𝑔,𝑖,𝑤

Detailed syntax breakdown of Definition df-wwlks
StepHypRef Expression
1 cwwlks 41028 . 2 class WWalkS
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1474 . . . . . 6 class 𝑤
6 c0 3874 . . . . . 6 class
75, 6wne 2780 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1474 . . . . . . . . 9 class 𝑖
109, 5cfv 5804 . . . . . . . 8 class (𝑤𝑖)
11 c1 9816 . . . . . . . . . 10 class 1
12 caddc 9818 . . . . . . . . . 10 class +
139, 11, 12co 6549 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 5804 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4127 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1474 . . . . . . . 8 class 𝑔
17 cedga 25792 . . . . . . . 8 class Edg
1816, 17cfv 5804 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 1977 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 9815 . . . . . . 7 class 0
21 chash 12979 . . . . . . . . 9 class #
225, 21cfv 5804 . . . . . . . 8 class (#‘𝑤)
23 cmin 10145 . . . . . . . 8 class
2422, 11, 23co 6549 . . . . . . 7 class ((#‘𝑤) − 1)
25 cfzo 12334 . . . . . . 7 class ..^
2620, 24, 25co 6549 . . . . . 6 class (0..^((#‘𝑤) − 1))
2719, 8, 26wral 2896 . . . . 5 wff 𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
287, 27wa 383 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))
29 cvtx 25673 . . . . . 6 class Vtx
3016, 29cfv 5804 . . . . 5 class (Vtx‘𝑔)
3130cword 13146 . . . 4 class Word (Vtx‘𝑔)
3228, 4, 31crab 2900 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))}
332, 3, 32cmpt 4643 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
341, 33wceq 1475 1 wff WWalkS = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
 Colors of variables: wff setvar class This definition is referenced by:  wwlks  41038
 Copyright terms: Public domain W3C validator