Definition df-clwwlk 27859

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 27652. 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 27858	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3410	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1538	. . . . . 6 class 𝑤
6		c0 4226	. . . . . 6 class ∅
7	5, 6	wne 2952	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1538	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6336	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 10569	. . . . . . . . . 10 class 1
12		caddc 10571	. . . . . . . . . 10 class +
13	9, 11, 12	co 7151	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6336	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4525	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1538	. . . . . . . 8 class 𝑔
17		cedg 26932	. . . . . . . 8 class Edg
18	16, 17	cfv 6336	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2112	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 10568	. . . . . . 7 class 0
21		chash 13733	. . . . . . . . 9 class ♯
22	5, 21	cfv 6336	. . . . . . . 8 class (♯‘𝑤)
23		cmin 10901	. . . . . . . 8 class −
24	22, 11, 23	co 7151	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13075	. . . . . . 7 class ..^
26	20, 24, 25	co 7151	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3071	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 13954	. . . . . . . 8 class lastS
29	5, 28	cfv 6336	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6336	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4525	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2112	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1085	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 26881	. . . . . 6 class Vtx
35	16, 34	cfv 6336	. . . . 5 class (Vtx‘𝑔)
36	35	cword 13906	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3075	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5113	. 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  27860