Definition df-clwwlk 30238

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 30025. 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 30237	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3457	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1562	. . . . . 6 class 𝑤
6		c0 4288	. . . . . 6 class ∅
7	5, 6	wne 2960	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1562	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6525	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11089	. . . . . . . . . 10 class 1
12		caddc 11091	. . . . . . . . . 10 class +
13	9, 11, 12	co 7400	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6525	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4587	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1562	. . . . . . . 8 class 𝑔
17		cedg 29302	. . . . . . . 8 class Edg
18	16, 17	cfv 6525	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2145	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11088	. . . . . . 7 class 0
21		chash 14354	. . . . . . . . 9 class ♯
22	5, 21	cfv 6525	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11429	. . . . . . . 8 class −
24	22, 11, 23	co 7400	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13670	. . . . . . 7 class ..^
26	20, 24, 25	co 7400	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3079	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14587	. . . . . . . 8 class lastS
29	5, 28	cfv 6525	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6525	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4587	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2145	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1101	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29251	. . . . . 6 class Vtx
35	16, 34	cfv 6525	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14538	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3417	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5185	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1563	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30239