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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwwlksn	$$class\mathrm{WWalksN}$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vg	$$setvarg$$
4		cvv	$$class\mathrm{V}$$
5		vw	$$setvarw$$
6		cwwlks	$$class\mathrm{WWalks}$$
7	3	cv	$$setvarg$$
8	7 6	cfv	$$class\mathrm{WWalks}\left(g\right)$$
9		chash	$$class\left|.\right|$$
10	5	cv	$$setvarw$$
11	10 9	cfv	$$class\left|w\right|$$
12	1	cv	$$setvarn$$
13		caddc	$$class+$$
14		c1	$$class1$$
15	12 14 13	co	$$class\left(n+1\right)$$
16	11 15	wceq	$$wff\left|w\right|=n+1$$
17	16 5 8	crab	$$class\left\{w\in \mathrm{WWalks}\left(g\right)|\left|w\right|=n+1\right\}$$
18	1 3 2 4 17	cmpo	$$class\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \mathrm{WWalks}\left(g\right)|\left|w\right|=n+1\right\}\right)$$
19	0 18	wceq	$$wff\mathrm{WWalksN}=\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \mathrm{WWalks}\left(g\right)|\left|w\right|=n+1\right\}\right)$$