Definition df-clwwlksn 41186

Description: Define the set of all closed walks (in an undirected graph) of a fixed length n 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 40977. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)

Assertion

Ref	Expression
df-clwwlksn	⊢ ClWWalkSN = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalkS‘𝑔) ∣ (#‘𝑤) = 𝑛})

Distinct variable group:   𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-clwwlksn

Step	Hyp	Ref	Expression
1		cclwwlksn 41184	. 2 class ClWWalkSN
2		vn	. . 3 setvar 𝑛
3		vg	. . 3 setvar 𝑔
4		cn 10897	. . 3 class ℕ
5		cvv 3173	. . 3 class V
6		vw	. . . . . . 7 setvar 𝑤
7	6	cv 1474	. . . . . 6 class 𝑤
8		chash 12979	. . . . . 6 class #
9	7, 8	cfv 5804	. . . . 5 class (#‘𝑤)
10	2	cv 1474	. . . . 5 class 𝑛
11	9, 10	wceq 1475	. . . 4 wff (#‘𝑤) = 𝑛
12	3	cv 1474	. . . . 5 class 𝑔
13		cclwwlks 41183	. . . . 5 class ClWWalkS
14	12, 13	cfv 5804	. . . 4 class (ClWWalkS‘𝑔)
15	11, 6, 14	crab 2900	. . 3 class {𝑤 ∈ (ClWWalkS‘𝑔) ∣ (#‘𝑤) = 𝑛}
16	2, 3, 4, 5, 15	cmpt2 6551	. 2 class (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalkS‘𝑔) ∣ (#‘𝑤) = 𝑛})
17	1, 16	wceq 1475	1 wff ClWWalkSN = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalkS‘𝑔) ∣ (#‘𝑤) = 𝑛})

This definition is referenced by:  clwwlksn  41189  clwwlknbp0  41192