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	⊢ ClWWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclwwlkn	⊢ ClWWalksN
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vg	⊢ 𝑔
4		cvv	⊢ V
5		vw	⊢ 𝑤
6		cclwwlk	⊢ ClWWalks
7	3	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( ClWWalks ‘ 𝑔 )
9		chash	⊢ ♯
10	5	cv	⊢ 𝑤
11	10 9	cfv	⊢ ( ♯ ‘ 𝑤 )
12	1	cv	⊢ 𝑛
13	11 12	wceq	⊢ ( ♯ ‘ 𝑤 ) = 𝑛
14	13 5 8	crab	⊢ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 }
15	1 3 2 4 14	cmpo	⊢ ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } )
16	0 15	wceq	⊢ ClWWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } )