Metamath Proof Explorer

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=g∈V⟼v∈Vtx⁡g,n∈ℕ0⟼w∈nClWWalksNg|w⁡0=v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclwwlknon classClWWalksNOn
1 vg setvarg
2 cvv classV
3 vv setvarv
4 cvtx classVtx
5 1 cv setvarg
6 5 4 cfv classVtx⁡g
7 vn setvarn
8 cn0 classℕ0
9 vw setvarw
10 7 cv setvarn
11 cclwwlkn classClWWalksN
12 10 5 11 co classnClWWalksNg
13 9 cv setvarw
14 cc0 class0
15 14 13 cfv classw⁡0
16 3 cv setvarv
17 15 16 wceq wffw⁡0=v
18 17 9 12 crab classw∈nClWWalksNg|w⁡0=v
19 3 7 6 8 18 cmpo classv∈Vtx⁡g,n∈ℕ0⟼w∈nClWWalksNg|w⁡0=v
20 1 2 19 cmpt classg∈V⟼v∈Vtx⁡g,n∈ℕ0⟼w∈nClWWalksNg|w⁡0=v
21 0 20 wceq wffClWWalksNOn=g∈V⟼v∈Vtx⁡g,n∈ℕ0⟼w∈nClWWalksNg|w⁡0=v