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

Definition df-wwlks 27619
 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 27392. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 27413. (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 27614 . 2 class WWalks
2 vg . . 3 setvar 𝑔
3 cvv 3444 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1537 . . . . . 6 class 𝑤
6 c0 4246 . . . . . 6 class
75, 6wne 2990 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1537 . . . . . . . . 9 class 𝑖
109, 5cfv 6328 . . . . . . . 8 class (𝑤𝑖)
11 c1 10531 . . . . . . . . . 10 class 1
12 caddc 10533 . . . . . . . . . 10 class +
139, 11, 12co 7139 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 6328 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4530 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1537 . . . . . . . 8 class 𝑔
17 cedg 26843 . . . . . . . 8 class Edg
1816, 17cfv 6328 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 2112 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 10530 . . . . . . 7 class 0
21 chash 13690 . . . . . . . . 9 class
225, 21cfv 6328 . . . . . . . 8 class (♯‘𝑤)
23 cmin 10863 . . . . . . . 8 class
2422, 11, 23co 7139 . . . . . . 7 class ((♯‘𝑤) − 1)
25 cfzo 13032 . . . . . . 7 class ..^
2620, 24, 25co 7139 . . . . . 6 class (0..^((♯‘𝑤) − 1))
2719, 8, 26wral 3109 . . . . 5 wff 𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
287, 27wa 399 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))
29 cvtx 26792 . . . . . 6 class Vtx
3016, 29cfv 6328 . . . . 5 class (Vtx‘𝑔)
3130cword 13861 . . . 4 class Word (Vtx‘𝑔)
3228, 4, 31crab 3113 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))}
332, 3, 32cmpt 5113 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
341, 33wceq 1538 1 wff WWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
 Colors of variables: wff setvar class This definition is referenced by:  wwlks  27624
 Copyright terms: Public domain W3C validator