Definition df-clwwlk 29911

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 29701. 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 29910	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3447	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1539	. . . . . 6 class 𝑤
6		c0 4296	. . . . . 6 class ∅
7	5, 6	wne 2925	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1539	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6511	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11069	. . . . . . . . . 10 class 1
12		caddc 11071	. . . . . . . . . 10 class +
13	9, 11, 12	co 7387	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6511	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4591	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1539	. . . . . . . 8 class 𝑔
17		cedg 28974	. . . . . . . 8 class Edg
18	16, 17	cfv 6511	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2109	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11068	. . . . . . 7 class 0
21		chash 14295	. . . . . . . . 9 class ♯
22	5, 21	cfv 6511	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11405	. . . . . . . 8 class −
24	22, 11, 23	co 7387	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13615	. . . . . . 7 class ..^
26	20, 24, 25	co 7387	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3044	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14527	. . . . . . . 8 class lastS
29	5, 28	cfv 6511	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6511	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4591	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2109	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1086	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 28923	. . . . . 6 class Vtx
35	16, 34	cfv 6511	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14478	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3405	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5188	. 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  29912