Definition df-clwwlk 30052

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 29839. 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 30051	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3429	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1541	. . . . . 6 class 𝑤
6		c0 4273	. . . . . 6 class ∅
7	5, 6	wne 2932	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1541	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6498	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11039	. . . . . . . . . 10 class 1
12		caddc 11041	. . . . . . . . . 10 class +
13	9, 11, 12	co 7367	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6498	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4569	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1541	. . . . . . . 8 class 𝑔
17		cedg 29116	. . . . . . . 8 class Edg
18	16, 17	cfv 6498	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2114	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11038	. . . . . . 7 class 0
21		chash 14292	. . . . . . . . 9 class ♯
22	5, 21	cfv 6498	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11377	. . . . . . . 8 class −
24	22, 11, 23	co 7367	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13608	. . . . . . 7 class ..^
26	20, 24, 25	co 7367	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3051	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14524	. . . . . . . 8 class lastS
29	5, 28	cfv 6498	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6498	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4569	. . . . . 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 29065	. . . . . 6 class Vtx
35	16, 34	cfv 6498	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14475	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3389	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5166	. 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  30053