Definition df-clwwlk 29232

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 29025. 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 29231	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3474	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1540	. . . . . 6 class 𝑤
6		c0 4322	. . . . . 6 class ∅
7	5, 6	wne 2940	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1540	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6543	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11110	. . . . . . . . . 10 class 1
12		caddc 11112	. . . . . . . . . 10 class +
13	9, 11, 12	co 7408	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6543	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4630	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1540	. . . . . . . 8 class 𝑔
17		cedg 28304	. . . . . . . 8 class Edg
18	16, 17	cfv 6543	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2106	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11109	. . . . . . 7 class 0
21		chash 14289	. . . . . . . . 9 class ♯
22	5, 21	cfv 6543	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11443	. . . . . . . 8 class −
24	22, 11, 23	co 7408	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13626	. . . . . . 7 class ..^
26	20, 24, 25	co 7408	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3061	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14511	. . . . . . . 8 class lastS
29	5, 28	cfv 6543	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6543	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4630	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2106	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1087	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 28253	. . . . . 6 class Vtx
35	16, 34	cfv 6543	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14463	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3432	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5231	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1541	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  29233