Definition df-clwwlk 30140

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 29927. 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 30139	. 2 class ClWWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3453	. . 3 class V
4		vw	. . . . . . 7 setvar 𝑤
5	4	cv 1558	. . . . . 6 class 𝑤
6		c0 4283	. . . . . 6 class ∅
7	5, 6	wne 2956	. . . . 5 wff 𝑤 ≠ ∅
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1558	. . . . . . . . 9 class 𝑖
10	9, 5	cfv 6515	. . . . . . . 8 class (𝑤‘𝑖)
11		c1 11067	. . . . . . . . . 10 class 1
12		caddc 11069	. . . . . . . . . 10 class +
13	9, 11, 12	co 7390	. . . . . . . . 9 class (𝑖 + 1)
14	13, 5	cfv 6515	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
15	10, 14	cpr 4581	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
16	2	cv 1558	. . . . . . . 8 class 𝑔
17		cedg 29204	. . . . . . . 8 class Edg
18	16, 17	cfv 6515	. . . . . . 7 class (Edg‘𝑔)
19	15, 18	wcel 2141	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20		cc0 11066	. . . . . . 7 class 0
21		chash 14336	. . . . . . . . 9 class ♯
22	5, 21	cfv 6515	. . . . . . . 8 class (♯‘𝑤)
23		cmin 11407	. . . . . . . 8 class −
24	22, 11, 23	co 7390	. . . . . . 7 class ((♯‘𝑤) − 1)
25		cfzo 13652	. . . . . . 7 class ..^
26	20, 24, 25	co 7390	. . . . . 6 class (0..^((♯‘𝑤) − 1))
27	19, 8, 26	wral 3075	. . . . 5 wff ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28		clsw 14568	. . . . . . . 8 class lastS
29	5, 28	cfv 6515	. . . . . . 7 class (lastS‘𝑤)
30	20, 5	cfv 6515	. . . . . . 7 class (𝑤‘0)
31	29, 30	cpr 4581	. . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
32	31, 18	wcel 2141	. . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
33	7, 27, 32	w3a 1097	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34		cvtx 29153	. . . . . 6 class Vtx
35	16, 34	cfv 6515	. . . . 5 class (Vtx‘𝑔)
36	35	cword 14519	. . . 4 class Word (Vtx‘𝑔)
37	33, 4, 36	crab 3413	. . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
38	2, 3, 37	cmpt 5178	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
39	1, 38	wceq 1559	1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})

This definition is referenced by:  clwwlk  30141