Definition df-clwwlk 28355

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 28148. 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 28354	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3433	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1538	. . . . . 6 class 𝑤
6		c0 4257	. . . . . 6 class ∅
7	5, 6	wne 2944	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1538	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6437	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 10881	. . . . . . . . . 10 class 1
12		caddc 10883	. . . . . . . . . 10 class +
13	9, 11, 12	co 7284	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6437	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4564	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1538	. . . . . . . 8 class 𝑔
17		cedg 27426	. . . . . . . 8 class Edg
18	16, 17	cfv 6437	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2107	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 10880	. . . . . . 7 class 0
21		chash 14053	. . . . . . . . 9 class ♯
22	5, 21	cfv 6437	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11214	. . . . . . . 8 class −
24	22, 11, 23	co 7284	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13391	. . . . . . 7 class ..^
26	20, 24, 25	co 7284	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3065	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14274	. . . . . . . 8 class lastS
29	5, 28	cfv 6437	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6437	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4564	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2107	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1086	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 27375	. . . . . 6 class Vtx
35	16, 34	cfv 6437	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14226	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3069	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5158	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1539	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  28356