Definition df-clwwlk 30460

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 30245. 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 30459	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3453	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1569	. . . . . 6 class 𝑤
6		c0 4282	. . . . . 6 class ∅
7	5, 6	wne 2957	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1569	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6537	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11129	. . . . . . . . . 10 class 1
12		caddc 11131	. . . . . . . . . 10 class +
13	9, 11, 12	co 7417	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6537	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4589	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1569	. . . . . . . 8 class 𝑔
17		cedg 29512	. . . . . . . 8 class Edg
18	16, 17	cfv 6537	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2145	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11128	. . . . . . 7 class 0
21		chash 14398	. . . . . . . . 9 class ♯
22	5, 21	cfv 6537	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11469	. . . . . . . 8 class −
24	22, 11, 23	co 7417	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13713	. . . . . . 7 class ..^
26	20, 24, 25	co 7417	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3078	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14631	. . . . . . . 8 class lastS
29	5, 28	cfv 6537	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6537	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4589	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2145	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1103	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29461	. . . . . 6 class Vtx
35	16, 34	cfv 6537	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14582	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3414	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5190	. 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 used by:  clwwlk  30461