Definition df-clwwlk 29973

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 29760. 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 29972	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3438	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1540	. . . . . 6 class 𝑤
6		c0 4284	. . . . . 6 class ∅
7	5, 6	wne 2930	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1540	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6489	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11017	. . . . . . . . . 10 class 1
12		caddc 11019	. . . . . . . . . 10 class +
13	9, 11, 12	co 7355	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6489	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4579	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1540	. . . . . . . 8 class 𝑔
17		cedg 29036	. . . . . . . 8 class Edg
18	16, 17	cfv 6489	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2113	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11016	. . . . . . 7 class 0
21		chash 14247	. . . . . . . . 9 class ♯
22	5, 21	cfv 6489	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11354	. . . . . . . 8 class −
24	22, 11, 23	co 7355	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13564	. . . . . . 7 class ..^
26	20, 24, 25	co 7355	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3049	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14479	. . . . . . . 8 class lastS
29	5, 28	cfv 6489	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6489	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4579	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2113	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1086	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 28985	. . . . . 6 class Vtx
35	16, 34	cfv 6489	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14430	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3397	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5176	. 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  29974