Definition df-clwwlk 29918

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 29708. 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 29917	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3450	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1539	. . . . . 6 class 𝑤
6		c0 4299	. . . . . 6 class ∅
7	5, 6	wne 2926	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1539	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6514	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11076	. . . . . . . . . 10 class 1
12		caddc 11078	. . . . . . . . . 10 class +
13	9, 11, 12	co 7390	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6514	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4594	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1539	. . . . . . . 8 class 𝑔
17		cedg 28981	. . . . . . . 8 class Edg
18	16, 17	cfv 6514	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2109	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11075	. . . . . . 7 class 0
21		chash 14302	. . . . . . . . 9 class ♯
22	5, 21	cfv 6514	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11412	. . . . . . . 8 class −
24	22, 11, 23	co 7390	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13622	. . . . . . 7 class ..^
26	20, 24, 25	co 7390	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3045	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14534	. . . . . . . 8 class lastS
29	5, 28	cfv 6514	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6514	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4594	. . . . . 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 28930	. . . . . 6 class Vtx
35	16, 34	cfv 6514	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14485	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3408	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5191	. 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  29919