Definition df-clwwlk 30362

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 30149. 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 30361	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3457	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1569	. . . . . 6 class 𝑤
6		c0 4286	. . . . . 6 class ∅
7	5, 6	wne 2960	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1569	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6540	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11112	. . . . . . . . . 10 class 1
12		caddc 11114	. . . . . . . . . 10 class +
13	9, 11, 12	co 7416	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6540	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4593	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1569	. . . . . . . 8 class 𝑔
17		cedg 29426	. . . . . . . 8 class Edg
18	16, 17	cfv 6540	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2146	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11111	. . . . . . 7 class 0
21		chash 14379	. . . . . . . . 9 class ♯
22	5, 21	cfv 6540	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11452	. . . . . . . 8 class −
24	22, 11, 23	co 7416	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13694	. . . . . . 7 class ..^
26	20, 24, 25	co 7416	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3081	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14612	. . . . . . . 8 class lastS
29	5, 28	cfv 6540	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6540	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4593	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2146	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1103	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29375	. . . . . 6 class Vtx
35	16, 34	cfv 6540	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14563	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3418	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5194	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1570	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is used by:  clwwlk  30363