Definition df-clwwlknon 30107

Description: Define the set of all closed walks a graph 𝑔, anchored at a fixed vertex 𝑣 (i.e., a walk starting and ending at the fixed vertex 𝑣, also called "a closed walk on vertex 𝑣") and having a fixed length 𝑛 as words over the set of vertices. Such a word corresponds to the sequence v=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)=v as defined in df-clwlks 29791. The set ((𝑣(ClWWalksNOn‘𝑔)𝑛) corresponds to the set of "walks from v to v of length n" in a statement of [Huneke] p. 2. (Contributed by AV, 24-Feb-2022.)

Assertion

Ref	Expression
df-clwwlknon	⊢ ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))

Distinct variable group:   𝑔,𝑛,𝑣,𝑤

Detailed syntax breakdown of Definition df-clwwlknon

Step	Hyp	Ref	Expression
1		cclwwlknon 30106	. 2 class ClWWalksNOn
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		vv	. . . 4 setvar 𝑣
5		vn	. . . 4 setvar 𝑛
6	2	cv 1539	. . . . 5 class 𝑔
7		cvtx 29013	. . . . 5 class Vtx
8	6, 7	cfv 6561	. . . 4 class (Vtx‘𝑔)
9		cn0 12526	. . . 4 class ℕ0
10		cc0 11155	. . . . . . 7 class 0
11		vw	. . . . . . . 8 setvar 𝑤
12	11	cv 1539	. . . . . . 7 class 𝑤
13	10, 12	cfv 6561	. . . . . 6 class (𝑤‘0)
14	4	cv 1539	. . . . . 6 class 𝑣
15	13, 14	wceq 1540	. . . . 5 wff (𝑤‘0) = 𝑣
16	5	cv 1539	. . . . . 6 class 𝑛
17		cclwwlkn 30043	. . . . . 6 class ClWWalksN
18	16, 6, 17	co 7431	. . . . 5 class (𝑛 ClWWalksN 𝑔)
19	15, 11, 18	crab 3436	. . . 4 class {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}
20	4, 5, 8, 9, 19	cmpo 7433	. . 3 class (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣})
21	2, 3, 20	cmpt 5225	. 2 class (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))
22	1, 21	wceq 1540	1 wff ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))

This definition is referenced by:  clwwlknonmpo  30108