MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clwwlknon Structured version   Visualization version   GIF version

Definition df-clwwlknon 27260
Description: Define the set of all closed walks a graph 𝑔, anchored at a fixed vertex 𝑣 (i.e., a walk starting and ending at the fixed vertex 𝑣, also called "a closed walk on vertex 𝑣") and having a fixed length 𝑛 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 26902. The set ((𝑣(ClWWalksNOn‘𝑔)𝑛) 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.)
Assertion
Ref Expression
df-clwwlknon ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))
Distinct variable group:   𝑔,𝑛,𝑣,𝑤

Detailed syntax breakdown of Definition df-clwwlknon
StepHypRef Expression
1 cclwwlknon 27259 . 2 class ClWWalksNOn
2 vg . . 3 setvar 𝑔
3 cvv 3351 . . 3 class V
4 vv . . . 4 setvar 𝑣
5 vn . . . 4 setvar 𝑛
62cv 1630 . . . . 5 class 𝑔
7 cvtx 26095 . . . . 5 class Vtx
86, 7cfv 6030 . . . 4 class (Vtx‘𝑔)
9 cn0 11499 . . . 4 class 0
10 cc0 10142 . . . . . . 7 class 0
11 vw . . . . . . . 8 setvar 𝑤
1211cv 1630 . . . . . . 7 class 𝑤
1310, 12cfv 6030 . . . . . 6 class (𝑤‘0)
144cv 1630 . . . . . 6 class 𝑣
1513, 14wceq 1631 . . . . 5 wff (𝑤‘0) = 𝑣
165cv 1630 . . . . . 6 class 𝑛
17 cclwwlkn 27174 . . . . . 6 class ClWWalksN
1816, 6, 17co 6796 . . . . 5 class (𝑛 ClWWalksN 𝑔)
1915, 11, 18crab 3065 . . . 4 class {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}
204, 5, 8, 9, 19cmpt2 6798 . . 3 class (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣})
212, 3, 20cmpt 4864 . 2 class (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))
221, 21wceq 1631 1 wff ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))
Colors of variables: wff setvar class
This definition is referenced by:  clwwlknonmpt2  27261
  Copyright terms: Public domain W3C validator