Definition df-clwwlk 29502

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 29295. 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 29501	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3472	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1538	. . . . . 6 class 𝑤
6		c0 4321	. . . . . 6 class ∅
7	5, 6	wne 2938	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1538	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6542	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11113	. . . . . . . . . 10 class 1
12		caddc 11115	. . . . . . . . . 10 class +
13	9, 11, 12	co 7411	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6542	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4629	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1538	. . . . . . . 8 class 𝑔
17		cedg 28574	. . . . . . . 8 class Edg
18	16, 17	cfv 6542	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2104	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11112	. . . . . . 7 class 0
21		chash 14294	. . . . . . . . 9 class ♯
22	5, 21	cfv 6542	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11448	. . . . . . . 8 class −
24	22, 11, 23	co 7411	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13631	. . . . . . 7 class ..^
26	20, 24, 25	co 7411	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3059	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14516	. . . . . . . 8 class lastS
29	5, 28	cfv 6542	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6542	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4629	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2104	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1085	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 28523	. . . . . 6 class Vtx
35	16, 34	cfv 6542	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14468	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3430	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5230	. 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  29503