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

Definition df-wwlk 25973
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-wlk 25802. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 25821. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
Assertion
Ref Expression
df-wwlk WWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)})
Distinct variable group:   𝑒,𝑖,𝑣,𝑤

Detailed syntax breakdown of Definition df-wwlk
StepHypRef Expression
1 cwwlk 25971 . 2 class WWalks
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3172 . . 3 class V
5 vw . . . . . . 7 setvar 𝑤
65cv 1473 . . . . . 6 class 𝑤
7 c0 3873 . . . . . 6 class
86, 7wne 2779 . . . . 5 wff 𝑤 ≠ ∅
9 vi . . . . . . . . . 10 setvar 𝑖
109cv 1473 . . . . . . . . 9 class 𝑖
1110, 6cfv 5790 . . . . . . . 8 class (𝑤𝑖)
12 c1 9793 . . . . . . . . . 10 class 1
13 caddc 9795 . . . . . . . . . 10 class +
1410, 12, 13co 6527 . . . . . . . . 9 class (𝑖 + 1)
1514, 6cfv 5790 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1611, 15cpr 4126 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
173cv 1473 . . . . . . . 8 class 𝑒
1817crn 5029 . . . . . . 7 class ran 𝑒
1916, 18wcel 1976 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒
20 cc0 9792 . . . . . . 7 class 0
21 chash 12934 . . . . . . . . 9 class #
226, 21cfv 5790 . . . . . . . 8 class (#‘𝑤)
23 cmin 10117 . . . . . . . 8 class
2422, 12, 23co 6527 . . . . . . 7 class ((#‘𝑤) − 1)
25 cfzo 12289 . . . . . . 7 class ..^
2620, 24, 25co 6527 . . . . . 6 class (0..^((#‘𝑤) − 1))
2719, 9, 26wral 2895 . . . . 5 wff 𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒
288, 27wa 382 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)
292cv 1473 . . . . 5 class 𝑣
3029cword 13092 . . . 4 class Word 𝑣
3128, 5, 30crab 2899 . . 3 class {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)}
322, 3, 4, 4, 31cmpt2 6529 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)})
331, 32wceq 1474 1 wff WWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)})
Colors of variables: wff setvar class
This definition is referenced by:  wwlk  25975  wwlkprop  25979
  Copyright terms: Public domain W3C validator