Definition df-clwwlk 29235

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 29028. 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 29234	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3475	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1541	. . . . . 6 class 𝑤
6		c0 4323	. . . . . 6 class ∅
7	5, 6	wne 2941	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1541	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6544	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11111	. . . . . . . . . 10 class 1
12		caddc 11113	. . . . . . . . . 10 class +
13	9, 11, 12	co 7409	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6544	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4631	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1541	. . . . . . . 8 class 𝑔
17		cedg 28307	. . . . . . . 8 class Edg
18	16, 17	cfv 6544	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2107	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11110	. . . . . . 7 class 0
21		chash 14290	. . . . . . . . 9 class ♯
22	5, 21	cfv 6544	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11444	. . . . . . . 8 class −
24	22, 11, 23	co 7409	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13627	. . . . . . 7 class ..^
26	20, 24, 25	co 7409	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3062	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14512	. . . . . . . 8 class lastS
29	5, 28	cfv 6544	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6544	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4631	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2107	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1088	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 28256	. . . . . 6 class Vtx
35	16, 34	cfv 6544	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14464	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3433	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5232	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1542	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  29236