Definition df-wwlksn

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 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwwlksn	|- WWalksN
1		vn	|- n
2		cn0	|- NN0
3		vg	|- g
4		cvv	|- _V
5		vw	|- w
6		cwwlks	|- WWalks
7	3	cv	|- g
8	7 6	cfv	|- ( WWalks ` g )
9		chash	|- #
10	5	cv	|- w
11	10 9	cfv	|- ( # ` w )
12	1	cv	|- n
13		caddc	|- +
14		c1	|- 1
15	12 14 13	co	|- ( n + 1 )
16	11 15	wceq	|- ( # ` w ) = ( n + 1 )
17	16 5 8	crab	|- { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) }
18	1 3 2 4 17	cmpo	|- ( n e. NN0 , g e. _V |-> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )
19	0 18	wceq	|- WWalksN = ( n e. NN0 , g e. _V |-> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )