Definition df-clwwlkn

Description: Define the set of all closed walks of a fixed length n as words over the set of vertices in a graph g . If 0 < n , such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlks . For n = 0 , the set is empty, see clwwlkn0 . (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 22-Mar-2022)

	Ref	Expression
Assertion	df-clwwlkn	$$⊢\mathrm{ClWWalksN}=\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \mathrm{ClWWalks}\left(g\right)|\left|w\right|=n\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclwwlkn	$$class\mathrm{ClWWalksN}$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vg	$$setvarg$$
4		cvv	$$class\mathrm{V}$$
5		vw	$$setvarw$$
6		cclwwlk	$$class\mathrm{ClWWalks}$$
7	3	cv	$$setvarg$$
8	7 6	cfv	$$class\mathrm{ClWWalks}\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	11 12	wceq	$$wff\left|w\right|=n$$
14	13 5 8	crab	$$class\left\{w\in \mathrm{ClWWalks}\left(g\right)|\left|w\right|=n\right\}$$
15	1 3 2 4 14	cmpo	$$class\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \mathrm{ClWWalks}\left(g\right)|\left|w\right|=n\right\}\right)$$
16	0 15	wceq	$$wff\mathrm{ClWWalksN}=\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \mathrm{ClWWalks}\left(g\right)|\left|w\right|=n\right\}\right)$$