Definition df-clwwlk 30067

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 29854. 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 30066	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3430	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1541	. . . . . 6 class 𝑤
6		c0 4274	. . . . . 6 class ∅
7	5, 6	wne 2933	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1541	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6492	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11030	. . . . . . . . . 10 class 1
12		caddc 11032	. . . . . . . . . 10 class +
13	9, 11, 12	co 7360	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6492	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4570	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1541	. . . . . . . 8 class 𝑔
17		cedg 29130	. . . . . . . 8 class Edg
18	16, 17	cfv 6492	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2114	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11029	. . . . . . 7 class 0
21		chash 14283	. . . . . . . . 9 class ♯
22	5, 21	cfv 6492	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11368	. . . . . . . 8 class −
24	22, 11, 23	co 7360	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13599	. . . . . . 7 class ..^
26	20, 24, 25	co 7360	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3052	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14515	. . . . . . . 8 class lastS
29	5, 28	cfv 6492	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6492	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4570	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2114	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1087	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29079	. . . . . 6 class Vtx
35	16, 34	cfv 6492	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14466	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3390	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5167	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1542	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30068