Definition df-clwwlk 30057

Description: Define the set of all closed 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) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlks 29844. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)

Assertion

Ref	Expression
df-clwwlk	⊢ ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

Distinct variable group:   𝑔,𝑖,𝑤

Detailed syntax breakdown of Definition df-clwwlk

Step	Hyp	Ref	Expression
1		cclwwlk 30056	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3440	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1540	. . . . . 6 class 𝑤
6		c0 4285	. . . . . 6 class ∅
7	5, 6	wne 2932	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1540	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6492	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11027	. . . . . . . . . 10 class 1
12		caddc 11029	. . . . . . . . . 10 class +
13	9, 11, 12	co 7358	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6492	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4582	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1540	. . . . . . . 8 class 𝑔
17		cedg 29120	. . . . . . . 8 class Edg
18	16, 17	cfv 6492	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2113	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11026	. . . . . . 7 class 0
21		chash 14253	. . . . . . . . 9 class ♯
22	5, 21	cfv 6492	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11364	. . . . . . . 8 class −
24	22, 11, 23	co 7358	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13570	. . . . . . 7 class ..^
26	20, 24, 25	co 7358	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3051	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14485	. . . . . . . 8 class lastS
29	5, 28	cfv 6492	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6492	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4582	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2113	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1086	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29069	. . . . . 6 class Vtx
35	16, 34	cfv 6492	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14436	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3399	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5179	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1541	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30058