Definition df-clwwlkn 16345

Description: Define the set of all closed walks of a fixed length n as words over the set of vertices in a graph g. If 0 < n, 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) . For n = 0, the set is empty, see clwwlkn0 16349. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)

Assertion

Ref	Expression
df-clwwlkn	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )

Distinct variable group:   g, n, w

Detailed syntax breakdown of Definition df-clwwlkn

Step	Hyp	Ref	Expression
1		cclwwlkn 16344	. 2 class ClWWalksN
2		vn	. . 3 setvar n
3		vg	. . 3 setvar g
4		cn0 9461	. . 3 class NN0
5		cvv 2803	. . 3 class _V
6		vw	. . . . . . 7 setvar w
7	6	cv 1397	. . . . . 6 class w
8		chash 11100	. . . . . 6 class ♯
9	7, 8	cfv 5333	. . . . 5 class (♯ ` w )
10	2	cv 1397	. . . . 5 class n
11	9, 10	wceq 1398	. . . 4 wff (♯ ` w ) = n
12	3	cv 1397	. . . . 5 class g
13		cclwwlk 16332	. . . . 5 class ClWWalks
14	12, 13	cfv 5333	. . . 4 class (ClWWalks ` g )
15	11, 6, 14	crab 2515	. . 3 class { w e. (ClWWalks ` g ) | (♯ ` w ) = n }
16	2, 3, 4, 5, 15	cmpo 6030	. 2 class ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
17	1, 16	wceq 1398	1 wff ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )

This definition is referenced by:  clwwlkng  16346  isclwwlkng  16347  isclwwlkni  16348  clwwlkn0  16349  clwwlknnn  16353  clwwlknon  16370