Definition df-clwwlk 30001

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 29791. 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 30000	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1539	. . . . . 6 class 𝑤
6		c0 4333	. . . . . 6 class ∅
7	5, 6	wne 2940	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1539	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6561	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11156	. . . . . . . . . 10 class 1
12		caddc 11158	. . . . . . . . . 10 class +
13	9, 11, 12	co 7431	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6561	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4628	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1539	. . . . . . . 8 class 𝑔
17		cedg 29064	. . . . . . . 8 class Edg
18	16, 17	cfv 6561	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2108	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11155	. . . . . . 7 class 0
21		chash 14369	. . . . . . . . 9 class ♯
22	5, 21	cfv 6561	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11492	. . . . . . . 8 class −
24	22, 11, 23	co 7431	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13694	. . . . . . 7 class ..^
26	20, 24, 25	co 7431	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3061	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14600	. . . . . . . 8 class lastS
29	5, 28	cfv 6561	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6561	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4628	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2108	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1087	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29013	. . . . . 6 class Vtx
35	16, 34	cfv 6561	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14552	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3436	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5225	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1540	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30002