Definition df-wwlksn 26723

Description: Define the set of all 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) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 26495. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)

Assertion

Ref	Expression
df-wwlksn	|- WWalksN = ( n e. NN0 , g e. _V |-> { w e. (WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )

Distinct variable group:   g, n, w

Detailed syntax breakdown of Definition df-wwlksn

Step	Hyp	Ref	Expression
1		cwwlksn 26718	. 2 class WWalksN
2		vn	. . 3 setvar n
3		vg	. . 3 setvar g
4		cn0 11292	. . 3 class NN0
5		cvv 3200	. . 3 class _V
6		vw	. . . . . . 7 setvar w
7	6	cv 1482	. . . . . 6 class w
8		chash 13117	. . . . . 6 class #
9	7, 8	cfv 5888	. . . . 5 class ( # ` w )
10	2	cv 1482	. . . . . 6 class n
11		c1 9937	. . . . . 6 class 1
12		caddc 9939	. . . . . 6 class +
13	10, 11, 12	co 6650	. . . . 5 class ( n + 1 )
14	9, 13	wceq 1483	. . . 4 wff ( # ` w ) = ( n + 1 )
15	3	cv 1482	. . . . 5 class g
16		cwwlks 26717	. . . . 5 class WWalks
17	15, 16	cfv 5888	. . . 4 class (WWalks ` g )
18	14, 6, 17	crab 2916	. . 3 class { w e. (WWalks ` g ) | ( # ` w ) = ( n + 1 ) }
19	2, 3, 4, 5, 18	cmpt2 6652	. 2 class ( n e. NN0 , g e. _V |-> { w e. (WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )
20	1, 19	wceq 1483	1 wff WWalksN = ( n e. NN0 , g e. _V |-> { w e. (WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )

This definition is referenced by:  wwlksn  26729  wwlknbp  26733  wspthsn  26735  iswwlksnon  26740