Definition df-clwwlknon 16212

Description: Define the set of all closed walks a graph g, anchored at a fixed vertex v (i.e., a walk starting and ending at the fixed vertex v, also called "a closed walk on vertex v") and having a fixed length n 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 . The set ( ( v (ClWWalksNOn ` g ) n ) 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 = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )

Distinct variable group:   g, n, v, w

Detailed syntax breakdown of Definition df-clwwlknon

Step	Hyp	Ref	Expression
1		cclwwlknon 16211	. 2 class ClWWalksNOn
2		vg	. . 3 setvar g
3		cvv 2800	. . 3 class _V
4		vv	. . . 4 setvar v
5		vn	. . . 4 setvar n
6	2	cv 1394	. . . . 5 class g
7		cvtx 15850	. . . . 5 class Vtx
8	6, 7	cfv 5322	. . . 4 class (Vtx ` g )
9		cn0 9390	. . . 4 class NN0
10		cc0 8020	. . . . . . 7 class 0
11		vw	. . . . . . . 8 setvar w
12	11	cv 1394	. . . . . . 7 class w
13	10, 12	cfv 5322	. . . . . 6 class ( w ` 0 )
14	4	cv 1394	. . . . . 6 class v
15	13, 14	wceq 1395	. . . . 5 wff ( w ` 0 ) = v
16	5	cv 1394	. . . . . 6 class n
17		cclwwlkn 16188	. . . . . 6 class ClWWalksN
18	16, 6, 17	co 6011	. . . . 5 class ( n ClWWalksN g )
19	15, 11, 18	crab 2512	. . . 4 class { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v }
20	4, 5, 8, 9, 19	cmpo 6013	. . 3 class ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } )
21	2, 3, 20	cmpt 4146	. 2 class ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
22	1, 21	wceq 1395	1 wff ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )

This definition is referenced by:  clwwlknonmpo  16213