Definition df-clwwlk 30630

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 30415. 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 30629	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3454	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1569	. . . . . 6 class 𝑤
6		c0 4281	. . . . . 6 class ∅
7	5, 6	wne 2959	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1569	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6566	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11240	. . . . . . . . . 10 class 1
12		caddc 11242	. . . . . . . . . 10 class +
13	9, 11, 12	co 7451	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6566	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4590	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1569	. . . . . . . 8 class 𝑔
17		cedg 29682	. . . . . . . 8 class Edg
18	16, 17	cfv 6566	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2147	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11239	. . . . . . 7 class 0
21		chash 14515	. . . . . . . . 9 class ♯
22	5, 21	cfv 6566	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11580	. . . . . . . 8 class −
24	22, 11, 23	co 7451	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13828	. . . . . . 7 class ..^
26	20, 24, 25	co 7451	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3080	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14748	. . . . . . . 8 class lastS
29	5, 28	cfv 6566	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6566	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4590	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2147	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1103	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29631	. . . . . 6 class Vtx
35	16, 34	cfv 6566	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14699	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3416	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5192	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1570	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is used by:  clwwlk  30631