Definition df-wspthsn 26725

Description: Define the collection of simple paths of a fixed length as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)

Assertion

Ref	Expression
df-wspthsn	|- WSPathsN = ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f (SPaths ` g ) w } )

Distinct variable group:   f, g, n, w

Detailed syntax breakdown of Definition df-wspthsn

Step	Hyp	Ref	Expression
1		cwwspthsn 26720	. 2 class WSPathsN
2		vn	. . 3 setvar n
3		vg	. . 3 setvar g
4		cn0 11292	. . 3 class NN0
5		cvv 3200	. . 3 class _V
6		vf	. . . . . . 7 setvar f
7	6	cv 1482	. . . . . 6 class f
8		vw	. . . . . . 7 setvar w
9	8	cv 1482	. . . . . 6 class w
10	3	cv 1482	. . . . . . 7 class g
11		cspths 26609	. . . . . . 7 class SPaths
12	10, 11	cfv 5888	. . . . . 6 class (SPaths ` g )
13	7, 9, 12	wbr 4653	. . . . 5 wff f (SPaths ` g ) w
14	13, 6	wex 1704	. . . 4 wff E. f f (SPaths ` g ) w
15	2	cv 1482	. . . . 5 class n
16		cwwlksn 26718	. . . . 5 class WWalksN
17	15, 10, 16	co 6650	. . . 4 class ( n WWalksN g )
18	14, 8, 17	crab 2916	. . 3 class { w e. ( n WWalksN g ) | E. f f (SPaths ` g ) w }
19	2, 3, 4, 5, 18	cmpt2 6652	. 2 class ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f (SPaths ` g ) w } )
20	1, 19	wceq 1483	1 wff WSPathsN = ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f (SPaths ` g ) w } )

This definition is referenced by:  wspthsn  26735  wspthnp  26737  wspn0  26820