Users' Mathboxes 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 41031
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 40798. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 25817. (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 41026 . 2 class WWalkS
2 vg . . 3 setvar 𝑔
3 cvv 3168 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1473 . . . . . 6 class 𝑤
6 c0 3869 . . . . . 6 class
75, 6wne 2775 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1473 . . . . . . . . 9 class 𝑖
109, 5cfv 5786 . . . . . . . 8 class (𝑤𝑖)
11 c1 9789 . . . . . . . . . 10 class 1
12 caddc 9791 . . . . . . . . . 10 class +
139, 11, 12co 6523 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 5786 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4122 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1473 . . . . . . . 8 class 𝑔
17 cedga 40349 . . . . . . . 8 class Edg
1816, 17cfv 5786 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 1975 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 9788 . . . . . . 7 class 0
21 chash 12930 . . . . . . . . 9 class #
225, 21cfv 5786 . . . . . . . 8 class (#‘𝑤)
23 cmin 10113 . . . . . . . 8 class
2422, 11, 23co 6523 . . . . . . 7 class ((#‘𝑤) − 1)
25 cfzo 12285 . . . . . . 7 class ..^
2620, 24, 25co 6523 . . . . . 6 class (0..^((#‘𝑤) − 1))
2719, 8, 26wral 2891 . . . . 5 wff 𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
287, 27wa 382 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))
29 cvtx 40227 . . . . . 6 class Vtx
3016, 29cfv 5786 . . . . 5 class (Vtx‘𝑔)
3130cword 13088 . . . 4 class Word (Vtx‘𝑔)
3228, 4, 31crab 2895 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))}
332, 3, 32cmpt 4633 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
341, 33wceq 1474 1 wff WWalkS = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
Colors of variables: wff setvar class
This definition is referenced by:  wwlks  41036
  Copyright terms: Public domain W3C validator