Definition df-clwwlk 30077

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 29864. 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 30076	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3432	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1546	. . . . . 6 class 𝑤
6		c0 4268	. . . . . 6 class ∅
7	5, 6	wne 2935	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1546	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6492	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11037	. . . . . . . . . 10 class 1
12		caddc 11039	. . . . . . . . . 10 class +
13	9, 11, 12	co 7363	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6492	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4564	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1546	. . . . . . . 8 class 𝑔
17		cedg 29141	. . . . . . . 8 class Edg
18	16, 17	cfv 6492	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2119	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11036	. . . . . . 7 class 0
21		chash 14290	. . . . . . . . 9 class ♯
22	5, 21	cfv 6492	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11375	. . . . . . . 8 class −
24	22, 11, 23	co 7363	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13606	. . . . . . 7 class ..^
26	20, 24, 25	co 7363	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3054	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14522	. . . . . . . 8 class lastS
29	5, 28	cfv 6492	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6492	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4564	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2119	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1092	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29090	. . . . . 6 class Vtx
35	16, 34	cfv 6492	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14473	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3392	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5160	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1547	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30078