Definition df-clwwlk 30014

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 29807. 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 30013	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3488	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1536	. . . . . 6 class 𝑤
6		c0 4352	. . . . . 6 class ∅
7	5, 6	wne 2946	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1536	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6573	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11185	. . . . . . . . . 10 class 1
12		caddc 11187	. . . . . . . . . 10 class +
13	9, 11, 12	co 7448	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6573	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4650	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1536	. . . . . . . 8 class 𝑔
17		cedg 29082	. . . . . . . 8 class Edg
18	16, 17	cfv 6573	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2108	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11184	. . . . . . 7 class 0
21		chash 14379	. . . . . . . . 9 class ♯
22	5, 21	cfv 6573	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11520	. . . . . . . 8 class −
24	22, 11, 23	co 7448	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13711	. . . . . . 7 class ..^
26	20, 24, 25	co 7448	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3067	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14610	. . . . . . . 8 class lastS
29	5, 28	cfv 6573	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6573	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4650	. . . . . 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 29031	. . . . . 6 class Vtx
35	16, 34	cfv 6573	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14562	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3443	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5249	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1537	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30015