Definition df-wspthsn

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwwspthsn	|- WSPathsN
1		vn	|- n
2		cn0	|- NN0
3		vg	|- g
4		cvv	|- _V
5		vw	|- w
6	1	cv	|- n
7		cwwlksn	|- WWalksN
8	3	cv	|- g
9	6 8 7	co	|- ( n WWalksN g )
10		vf	|- f
11	10	cv	|- f
12		cspths	|- SPaths
13	8 12	cfv	|- ( SPaths ` g )
14	5	cv	|- w
15	11 14 13	wbr	|- f ( SPaths ` g ) w
16	15 10	wex	|- E. f f ( SPaths ` g ) w
17	16 5 9	crab	|- { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w }
18	1 3 2 4 17	cmpo	|- ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } )
19	0 18	wceq	|- WSPathsN = ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } )