Definition df-clwwlk 27754

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 27546. 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 27753	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3494	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1532	. . . . . 6 class 𝑤
6		c0 4290	. . . . . 6 class ∅
7	5, 6	wne 3016	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1532	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6349	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 10532	. . . . . . . . . 10 class 1
12		caddc 10534	. . . . . . . . . 10 class +
13	9, 11, 12	co 7150	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6349	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4562	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1532	. . . . . . . 8 class 𝑔
17		cedg 26826	. . . . . . . 8 class Edg
18	16, 17	cfv 6349	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2110	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 10531	. . . . . . 7 class 0
21		chash 13684	. . . . . . . . 9 class ♯
22	5, 21	cfv 6349	. . . . . . . 8 class (♯‘𝑤)
23		cmin 10864	. . . . . . . 8 class −
24	22, 11, 23	co 7150	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13027	. . . . . . 7 class ..^
26	20, 24, 25	co 7150	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3138	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 13908	. . . . . . . 8 class lastS
29	5, 28	cfv 6349	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6349	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4562	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2110	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1083	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 26775	. . . . . 6 class Vtx
35	16, 34	cfv 6349	. . . . 5 class (Vtx‘𝑔)
36	35	cword 13855	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3142	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5138	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1533	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  27755