MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wwlks Structured version   Visualization version   GIF version

Definition df-wwlks 27535
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 27308. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 27329. (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 27530 . 2 class WWalks
2 vg . . 3 setvar 𝑔
3 cvv 3492 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1527 . . . . . 6 class 𝑤
6 c0 4288 . . . . . 6 class
75, 6wne 3013 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1527 . . . . . . . . 9 class 𝑖
109, 5cfv 6348 . . . . . . . 8 class (𝑤𝑖)
11 c1 10526 . . . . . . . . . 10 class 1
12 caddc 10528 . . . . . . . . . 10 class +
139, 11, 12co 7145 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 6348 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4559 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1527 . . . . . . . 8 class 𝑔
17 cedg 26759 . . . . . . . 8 class Edg
1816, 17cfv 6348 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 2105 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 10525 . . . . . . 7 class 0
21 chash 13678 . . . . . . . . 9 class
225, 21cfv 6348 . . . . . . . 8 class (♯‘𝑤)
23 cmin 10858 . . . . . . . 8 class
2422, 11, 23co 7145 . . . . . . 7 class ((♯‘𝑤) − 1)
25 cfzo 13021 . . . . . . 7 class ..^
2620, 24, 25co 7145 . . . . . 6 class (0..^((♯‘𝑤) − 1))
2719, 8, 26wral 3135 . . . . 5 wff 𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
287, 27wa 396 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))
29 cvtx 26708 . . . . . 6 class Vtx
3016, 29cfv 6348 . . . . 5 class (Vtx‘𝑔)
3130cword 13849 . . . 4 class Word (Vtx‘𝑔)
3228, 4, 31crab 3139 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))}
332, 3, 32cmpt 5137 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
341, 33wceq 1528 1 wff WWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
Colors of variables: wff setvar class
This definition is referenced by:  wwlks  27540
  Copyright terms: Public domain W3C validator