Definition df-clwwlk 28247

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 28040. 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 28246	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3422	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1538	. . . . . 6 class 𝑤
6		c0 4253	. . . . . 6 class ∅
7	5, 6	wne 2942	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1538	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6418	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 10803	. . . . . . . . . 10 class 1
12		caddc 10805	. . . . . . . . . 10 class +
13	9, 11, 12	co 7255	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6418	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4560	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1538	. . . . . . . 8 class 𝑔
17		cedg 27320	. . . . . . . 8 class Edg
18	16, 17	cfv 6418	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2108	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 10802	. . . . . . 7 class 0
21		chash 13972	. . . . . . . . 9 class ♯
22	5, 21	cfv 6418	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11135	. . . . . . . 8 class −
24	22, 11, 23	co 7255	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13311	. . . . . . 7 class ..^
26	20, 24, 25	co 7255	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3063	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14193	. . . . . . . 8 class lastS
29	5, 28	cfv 6418	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6418	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4560	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2108	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1085	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 27269	. . . . . 6 class Vtx
35	16, 34	cfv 6418	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14145	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3067	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5153	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1539	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  28248