Definition df-clwwlk 29960

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 29750. 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 29959	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3436	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1540	. . . . . 6 class 𝑤
6		c0 4283	. . . . . 6 class ∅
7	5, 6	wne 2928	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1540	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6481	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11007	. . . . . . . . . 10 class 1
12		caddc 11009	. . . . . . . . . 10 class +
13	9, 11, 12	co 7346	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6481	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4578	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1540	. . . . . . . 8 class 𝑔
17		cedg 29026	. . . . . . . 8 class Edg
18	16, 17	cfv 6481	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2111	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11006	. . . . . . 7 class 0
21		chash 14237	. . . . . . . . 9 class ♯
22	5, 21	cfv 6481	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11344	. . . . . . . 8 class −
24	22, 11, 23	co 7346	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13554	. . . . . . 7 class ..^
26	20, 24, 25	co 7346	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3047	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14469	. . . . . . . 8 class lastS
29	5, 28	cfv 6481	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6481	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4578	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2111	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1086	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 28975	. . . . . 6 class Vtx
35	16, 34	cfv 6481	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14420	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3395	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5172	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1541	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  29961