Definition df-clwwlk 29944

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 29734. 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 29943	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3438	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1539	. . . . . 6 class 𝑤
6		c0 4286	. . . . . 6 class ∅
7	5, 6	wne 2925	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1539	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6486	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11029	. . . . . . . . . 10 class 1
12		caddc 11031	. . . . . . . . . 10 class +
13	9, 11, 12	co 7353	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6486	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4581	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1539	. . . . . . . 8 class 𝑔
17		cedg 29010	. . . . . . . 8 class Edg
18	16, 17	cfv 6486	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2109	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11028	. . . . . . 7 class 0
21		chash 14255	. . . . . . . . 9 class ♯
22	5, 21	cfv 6486	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11365	. . . . . . . 8 class −
24	22, 11, 23	co 7353	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13575	. . . . . . 7 class ..^
26	20, 24, 25	co 7353	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3044	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14487	. . . . . . . 8 class lastS
29	5, 28	cfv 6486	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6486	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4581	. . . . . 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 28959	. . . . . 6 class Vtx
35	16, 34	cfv 6486	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14438	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3396	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5176	. 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  29945