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 26854
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 26626. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 26647. (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 26849 . 2 class WWalks
2 vg . . 3 setvar 𝑔
3 cvv 3304 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1595 . . . . . 6 class 𝑤
6 c0 4023 . . . . . 6 class
75, 6wne 2896 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1595 . . . . . . . . 9 class 𝑖
109, 5cfv 6001 . . . . . . . 8 class (𝑤𝑖)
11 c1 10050 . . . . . . . . . 10 class 1
12 caddc 10052 . . . . . . . . . 10 class +
139, 11, 12co 6765 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 6001 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4287 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1595 . . . . . . . 8 class 𝑔
17 cedg 26059 . . . . . . . 8 class Edg
1816, 17cfv 6001 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 2103 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 10049 . . . . . . 7 class 0
21 chash 13232 . . . . . . . . 9 class
225, 21cfv 6001 . . . . . . . 8 class (♯‘𝑤)
23 cmin 10379 . . . . . . . 8 class
2422, 11, 23co 6765 . . . . . . 7 class ((♯‘𝑤) − 1)
25 cfzo 12580 . . . . . . 7 class ..^
2620, 24, 25co 6765 . . . . . 6 class (0..^((♯‘𝑤) − 1))
2719, 8, 26wral 3014 . . . . 5 wff 𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
287, 27wa 383 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))
29 cvtx 25994 . . . . . 6 class Vtx
3016, 29cfv 6001 . . . . 5 class (Vtx‘𝑔)
3130cword 13398 . . . 4 class Word (Vtx‘𝑔)
3228, 4, 31crab 3018 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))}
332, 3, 32cmpt 4837 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
341, 33wceq 1596 1 wff WWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
Colors of variables: wff setvar class
This definition is referenced by:  wwlks  26859
  Copyright terms: Public domain W3C validator