Definition df-clwwlk 30010

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 29803. 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 30009	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3477	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1535	. . . . . 6 class 𝑤
6		c0 4338	. . . . . 6 class ∅
7	5, 6	wne 2937	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1535	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6562	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11153	. . . . . . . . . 10 class 1
12		caddc 11155	. . . . . . . . . 10 class +
13	9, 11, 12	co 7430	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6562	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4632	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1535	. . . . . . . 8 class 𝑔
17		cedg 29078	. . . . . . . 8 class Edg
18	16, 17	cfv 6562	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2105	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11152	. . . . . . 7 class 0
21		chash 14365	. . . . . . . . 9 class ♯
22	5, 21	cfv 6562	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11489	. . . . . . . 8 class −
24	22, 11, 23	co 7430	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13690	. . . . . . 7 class ..^
26	20, 24, 25	co 7430	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3058	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14596	. . . . . . . 8 class lastS
29	5, 28	cfv 6562	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6562	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4632	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2105	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1086	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29027	. . . . . 6 class Vtx
35	16, 34	cfv 6562	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14548	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3432	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5230	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1536	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30011