Definition df-clwwlknon

Description: Define the set of all closed walks a graph g , anchored at a fixed vertex v (i.e., a walk starting and ending at the fixed vertex v , also called "a closed walk on vertex v ") and having a fixed length n as words over the set of vertices. Such a word corresponds to the sequence v=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)=v as defined in df-clwlks . The set ( ( v ( ClWWalksNOng ) n ) corresponds to the set of "walks from v to v of length n" in a statement of Huneke p. 2. (Contributed by AV, 24-Feb-2022)

	Ref	Expression
Assertion	df-clwwlknon	⊢ ClWWalksNOn = ( 𝑔 ∈ V ↦ ( 𝑣 ∈ ( Vtx ‘ 𝑔 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝑔 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclwwlknon	⊢ ClWWalksNOn
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cvtx	⊢ Vtx
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Vtx ‘ 𝑔 )
7		vn	⊢ 𝑛
8		cn0	⊢ ℕ0
9		vw	⊢ 𝑤
10	7	cv	⊢ 𝑛
11		cclwwlkn	⊢ ClWWalksN
12	10 5 11	co	⊢ ( 𝑛 ClWWalksN 𝑔 )
13	9	cv	⊢ 𝑤
14		cc0	⊢ 0
15	14 13	cfv	⊢ ( 𝑤 ‘ 0 )
16	3	cv	⊢ 𝑣
17	15 16	wceq	⊢ ( 𝑤 ‘ 0 ) = 𝑣
18	17 9 12	crab	⊢ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝑔 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 }
19	3 7 6 8 18	cmpo	⊢ ( 𝑣 ∈ ( Vtx ‘ 𝑔 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝑔 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } )
20	1 2 19	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑣 ∈ ( Vtx ‘ 𝑔 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝑔 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
21	0 20	wceq	⊢ ClWWalksNOn = ( 𝑔 ∈ V ↦ ( 𝑣 ∈ ( Vtx ‘ 𝑔 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝑔 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )