Definition df-clwwlk 27767

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 27560. 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 27766	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3441	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1537	. . . . . 6 class 𝑤
6		c0 4243	. . . . . 6 class ∅
7	5, 6	wne 2987	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1537	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6324	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 10527	. . . . . . . . . 10 class 1
12		caddc 10529	. . . . . . . . . 10 class +
13	9, 11, 12	co 7135	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6324	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4527	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1537	. . . . . . . 8 class 𝑔
17		cedg 26840	. . . . . . . 8 class Edg
18	16, 17	cfv 6324	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2111	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 10526	. . . . . . 7 class 0
21		chash 13686	. . . . . . . . 9 class ♯
22	5, 21	cfv 6324	. . . . . . . 8 class (♯‘𝑤)
23		cmin 10859	. . . . . . . 8 class −
24	22, 11, 23	co 7135	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13028	. . . . . . 7 class ..^
26	20, 24, 25	co 7135	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3106	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 13905	. . . . . . . 8 class lastS
29	5, 28	cfv 6324	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6324	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4527	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2111	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1084	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 26789	. . . . . 6 class Vtx
35	16, 34	cfv 6324	. . . . 5 class (Vtx‘𝑔)
36	35	cword 13857	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3110	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5110	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1538	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  27768