Definition df-clwwlks 41185

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 40977. 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-clwwlks	⊢ ClWWalkS = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

Distinct variable group:   𝑔,𝑖,𝑤

Detailed syntax breakdown of Definition df-clwwlks

Step	Hyp	Ref	Expression
1		cclwwlks 41183	. 2 class ClWWalkS
2		vg	. . 3 setvar 𝑔
3		cvv 3173	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1474	. . . . . 6 class 𝑤
6		c0 3874	. . . . . 6 class ∅
7	5, 6	wne 2780	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1474	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 5804	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 9816	. . . . . . . . . 10 class 1
12		caddc 9818	. . . . . . . . . 10 class +
13	9, 11, 12	co 6549	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 5804	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4127	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1474	. . . . . . . 8 class 𝑔
17		cedga 25792	. . . . . . . 8 class Edg
18	16, 17	cfv 5804	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 1977	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 9815	. . . . . . 7 class 0
21		chash 12979	. . . . . . . . 9 class #
22	5, 21	cfv 5804	. . . . . . . 8 class (#‘𝑤)
23		cmin 10145	. . . . . . . 8 class −
24	22, 11, 23	co 6549	. . . . . . 7 class ((#‘𝑤) − 1)
25		cfzo 12334	. . . . . . 7 class ..^
26	20, 24, 25	co 6549	. . . . . 6 class (0..^((#‘𝑤) − 1))
27	19, 8, 26	wral 2896	. . . . 5 wff ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 13147	. . . . . . . 8 class lastS
29	5, 28	cfv 5804	. . . . . . 7 class ( lastS ‘𝑤)
30	20, 5	cfv 5804	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4127	. . . . . 6 class {( lastS ‘𝑤), (𝑤‘0)}
32	31, 18	wcel 1977	. . . . 5 wff {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1031	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 25673	. . . . . 6 class Vtx
35	16, 34	cfv 5804	. . . . 5 class (Vtx‘𝑔)
36	35	cword 13146	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 2900	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 4643	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1475	1 wff ClWWalkS = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlks  41187