Definition df-wwlks 28096

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 27869. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 27890. (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

Step	Hyp	Ref	Expression
1		cwwlks 28091	. 2 class WWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3422	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1538	. . . . . 6 class 𝑤
6		c0 4253	. . . . . 6 class ∅
7	5, 6	wne 2942	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1538	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6418	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 10803	. . . . . . . . . 10 class 1
12		caddc 10805	. . . . . . . . . 10 class +
13	9, 11, 12	co 7255	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6418	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4560	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1538	. . . . . . . 8 class 𝑔
17		cedg 27320	. . . . . . . 8 class Edg
18	16, 17	cfv 6418	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2108	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 10802	. . . . . . 7 class 0
21		chash 13972	. . . . . . . . 9 class ♯
22	5, 21	cfv 6418	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11135	. . . . . . . 8 class −
24	22, 11, 23	co 7255	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13311	. . . . . . 7 class ..^
26	20, 24, 25	co 7255	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3063	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28	7, 27	wa 395	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))
29		cvtx 27269	. . . . . 6 class Vtx
30	16, 29	cfv 6418	. . . . 5 class (Vtx‘𝑔)
31	30	cword 14145	. . . 4 class Word (Vtx‘𝑔)
32	28, 4, 31	crab 3067	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))}
33	2, 3, 32	cmpt 5153	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
34	1, 33	wceq 1539	1 wff WWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})

This definition is referenced by:  wwlks  28101