Definition df-clwwlk 30314

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 30101. 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 30313	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3455	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1569	. . . . . 6 class 𝑤
6		c0 4287	. . . . . 6 class ∅
7	5, 6	wne 2958	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1569	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6538	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11102	. . . . . . . . . 10 class 1
12		caddc 11104	. . . . . . . . . 10 class +
13	9, 11, 12	co 7412	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6538	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4592	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1569	. . . . . . . 8 class 𝑔
17		cedg 29378	. . . . . . . 8 class Edg
18	16, 17	cfv 6538	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2143	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11101	. . . . . . 7 class 0
21		chash 14368	. . . . . . . . 9 class ♯
22	5, 21	cfv 6538	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11442	. . . . . . . 8 class −
24	22, 11, 23	co 7412	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13684	. . . . . . 7 class ..^
26	20, 24, 25	co 7412	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3079	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14601	. . . . . . . 8 class lastS
29	5, 28	cfv 6538	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6538	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4592	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2143	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1103	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29327	. . . . . 6 class Vtx
35	16, 34	cfv 6538	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14552	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3416	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5193	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1570	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30315