Definition df-clwwlk 29909

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 29699. 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 29908	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3459	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1539	. . . . . 6 class 𝑤
6		c0 4308	. . . . . 6 class ∅
7	5, 6	wne 2932	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1539	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6530	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11128	. . . . . . . . . 10 class 1
12		caddc 11130	. . . . . . . . . 10 class +
13	9, 11, 12	co 7403	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6530	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4603	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1539	. . . . . . . 8 class 𝑔
17		cedg 28972	. . . . . . . 8 class Edg
18	16, 17	cfv 6530	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2108	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11127	. . . . . . 7 class 0
21		chash 14346	. . . . . . . . 9 class ♯
22	5, 21	cfv 6530	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11464	. . . . . . . 8 class −
24	22, 11, 23	co 7403	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13669	. . . . . . 7 class ..^
26	20, 24, 25	co 7403	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3051	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14578	. . . . . . . 8 class lastS
29	5, 28	cfv 6530	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6530	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4603	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2108	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1086	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 28921	. . . . . 6 class Vtx
35	16, 34	cfv 6530	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14529	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3415	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5201	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1540	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  29910