Definition df-clwwlk 27762

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 27554. 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 27761	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3496	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1536	. . . . . 6 class 𝑤
6		c0 4293	. . . . . 6 class ∅
7	5, 6	wne 3018	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1536	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6357	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 10540	. . . . . . . . . 10 class 1
12		caddc 10542	. . . . . . . . . 10 class +
13	9, 11, 12	co 7158	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6357	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4571	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1536	. . . . . . . 8 class 𝑔
17		cedg 26834	. . . . . . . 8 class Edg
18	16, 17	cfv 6357	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2114	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 10539	. . . . . . 7 class 0
21		chash 13693	. . . . . . . . 9 class ♯
22	5, 21	cfv 6357	. . . . . . . 8 class (♯‘𝑤)
23		cmin 10872	. . . . . . . 8 class −
24	22, 11, 23	co 7158	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13036	. . . . . . 7 class ..^
26	20, 24, 25	co 7158	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3140	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 13916	. . . . . . . 8 class lastS
29	5, 28	cfv 6357	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6357	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4571	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2114	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1083	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 26783	. . . . . 6 class Vtx
35	16, 34	cfv 6357	. . . . 5 class (Vtx‘𝑔)
36	35	cword 13864	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3144	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5148	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1537	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  27763