Metamath Proof Explorer

Definition df-wwlks

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 . w = (/) has to be excluded because a walk always consists of at least one vertex, see wlkn0 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion df-wwlks ⊢ WWalks = g ∈ V ⟼ w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlks class WWalks
1 vg setvar g
2 cvv class V
3 vw setvar w
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx ⁡ g
7 6 cword class Word Vtx ⁡ g
8 3 cv setvar w
9 c0 class ∅
10 8 9 wne wff w ≠ ∅
11 vi setvar i
12 cc0 class 0
13 cfzo class ..^
14 chash class .
15 8 14 cfv class w
16 cmin class −
17 c1 class 1
18 15 17 16 co class w − 1
19 12 18 13 co class 0 ..^ w − 1
20 11 cv setvar i
21 20 8 cfv class w ⁡ i
22 caddc class +
23 20 17 22 co class i + 1
24 23 8 cfv class w ⁡ i + 1
25 21 24 cpr class w ⁡ i w ⁡ i + 1
26 cedg class Edg
27 5 26 cfv class Edg ⁡ g
28 25 27 wcel wff w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g
29 28 11 19 wral wff ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g
30 10 29 wa wff w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g
31 30 3 7 crab class w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g
32 1 2 31 cmpt class g ∈ V ⟼ w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g
33 0 32 wceq wff WWalks = g ∈ V ⟼ w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g