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	$$⊢\mathrm{WSPathsN}=\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \left(n\mathrm{WWalksN}g\right)|\exists ff\mathrm{SPaths}\left(g\right)w\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwwspthsn	$$class\mathrm{WSPathsN}$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vg	$$setvarg$$
4		cvv	$$class\mathrm{V}$$
5		vw	$$setvarw$$
6	1	cv	$$setvarn$$
7		cwwlksn	$$class\mathrm{WWalksN}$$
8	3	cv	$$setvarg$$
9	6 8 7	co	$$class\left(n\mathrm{WWalksN}g\right)$$
10		vf	$$setvarf$$
11	10	cv	$$setvarf$$
12		cspths	$$class\mathrm{SPaths}$$
13	8 12	cfv	$$class\mathrm{SPaths}\left(g\right)$$
14	5	cv	$$setvarw$$
15	11 14 13	wbr	$$wfff\mathrm{SPaths}\left(g\right)w$$
16	15 10	wex	$$wff\exists ff\mathrm{SPaths}\left(g\right)w$$
17	16 5 9	crab	$$class\left\{w\in \left(n\mathrm{WWalksN}g\right)|\exists ff\mathrm{SPaths}\left(g\right)w\right\}$$
18	1 3 2 4 17	cmpo	$$class\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \left(n\mathrm{WWalksN}g\right)|\exists ff\mathrm{SPaths}\left(g\right)w\right\}\right)$$
19	0 18	wceq	$$wff\mathrm{WSPathsN}=\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \left(n\mathrm{WWalksN}g\right)|\exists ff\mathrm{SPaths}\left(g\right)w\right\}\right)$$