Definition df-clwwlk 30579

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 30364. 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 30578	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3450	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1568	. . . . . 6 class 𝑤
6		c0 4278	. . . . . 6 class ∅
7	5, 6	wne 2955	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1568	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6539	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11205	. . . . . . . . . 10 class 1
12		caddc 11207	. . . . . . . . . 10 class +
13	9, 11, 12	co 7421	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6539	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4586	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1568	. . . . . . . 8 class 𝑔
17		cedg 29631	. . . . . . . 8 class Edg
18	16, 17	cfv 6539	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2144	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11204	. . . . . . 7 class 0
21		chash 14478	. . . . . . . . 9 class ♯
22	5, 21	cfv 6539	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11545	. . . . . . . 8 class −
24	22, 11, 23	co 7421	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13792	. . . . . . 7 class ..^
26	20, 24, 25	co 7421	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3076	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14711	. . . . . . . 8 class lastS
29	5, 28	cfv 6539	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6539	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4586	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2144	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1103	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29580	. . . . . 6 class Vtx
35	16, 34	cfv 6539	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14662	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3412	. . 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 1569	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is used by:  clwwlk  30580