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

Definition df-clwwlknon 27800
 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 27485. 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 27799 . 2 class ClWWalksNOn
2 vg . . 3 setvar 𝑔
3 cvv 3500 . . 3 class V
4 vv . . . 4 setvar 𝑣
5 vn . . . 4 setvar 𝑛
62cv 1529 . . . . 5 class 𝑔
7 cvtx 26714 . . . . 5 class Vtx
86, 7cfv 6354 . . . 4 class (Vtx‘𝑔)
9 cn0 11891 . . . 4 class 0
10 cc0 10531 . . . . . . 7 class 0
11 vw . . . . . . . 8 setvar 𝑤
1211cv 1529 . . . . . . 7 class 𝑤
1310, 12cfv 6354 . . . . . 6 class (𝑤‘0)
144cv 1529 . . . . . 6 class 𝑣
1513, 14wceq 1530 . . . . 5 wff (𝑤‘0) = 𝑣
165cv 1529 . . . . . 6 class 𝑛
17 cclwwlkn 27735 . . . . . 6 class ClWWalksN
1816, 6, 17co 7150 . . . . 5 class (𝑛 ClWWalksN 𝑔)
1915, 11, 18crab 3147 . . . 4 class {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}
204, 5, 8, 9, 19cmpo 7152 . . 3 class (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣})
212, 3, 20cmpt 5143 . 2 class (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))
221, 21wceq 1530 1 wff ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))
 Colors of variables: wff setvar class This definition is referenced by:  clwwlknonmpo  27801
 Copyright terms: Public domain W3C validator