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 ∈ n ClWWalksN g | w ⁡ 0 = v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclwwlknon class ClWWalksNOn
1 vg setvar g
2 cvv class V
3 vv setvar v
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx ⁡ g
7 vn setvar n
8 cn0 class ℕ 0
9 vw setvar w
10 7 cv setvar n
11 cclwwlkn class ClWWalksN
12 10 5 11 co class n ClWWalksN g
13 9 cv setvar w
14 cc0 class 0
15 14 13 cfv class w ⁡ 0
16 3 cv setvar v
17 15 16 wceq wff w ⁡ 0 = v
18 17 9 12 crab class w ∈ n ClWWalksN g | w ⁡ 0 = v
19 3 7 6 8 18 cmpo class v ∈ Vtx ⁡ g , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN g | w ⁡ 0 = v
20 1 2 19 cmpt class g ∈ V ⟼ v ∈ Vtx ⁡ g , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN g | w ⁡ 0 = v
21 0 20 wceq wff ClWWalksNOn = g ∈ V ⟼ v ∈ Vtx ⁡ g , n ∈ ℕ 0 ⟼ w ∈ n ClWWalksN g | w ⁡ 0 = v