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 29081
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 28768. 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 29080 . 2 class ClWWalksNOn
2 vg . . 3 setvar 𝑔
3 cvv 3447 . . 3 class V
4 vv . . . 4 setvar 𝑣
5 vn . . . 4 setvar 𝑛
62cv 1541 . . . . 5 class 𝑔
7 cvtx 27996 . . . . 5 class Vtx
86, 7cfv 6500 . . . 4 class (Vtxβ€˜π‘”)
9 cn0 12421 . . . 4 class β„•0
10 cc0 11059 . . . . . . 7 class 0
11 vw . . . . . . . 8 setvar 𝑀
1211cv 1541 . . . . . . 7 class 𝑀
1310, 12cfv 6500 . . . . . 6 class (π‘€β€˜0)
144cv 1541 . . . . . 6 class 𝑣
1513, 14wceq 1542 . . . . 5 wff (π‘€β€˜0) = 𝑣
165cv 1541 . . . . . 6 class 𝑛
17 cclwwlkn 29017 . . . . . 6 class ClWWalksN
1816, 6, 17co 7361 . . . . 5 class (𝑛 ClWWalksN 𝑔)
1915, 11, 18crab 3406 . . . 4 class {𝑀 ∈ (𝑛 ClWWalksN 𝑔) ∣ (π‘€β€˜0) = 𝑣}
204, 5, 8, 9, 19cmpo 7363 . . 3 class (𝑣 ∈ (Vtxβ€˜π‘”), 𝑛 ∈ β„•0 ↦ {𝑀 ∈ (𝑛 ClWWalksN 𝑔) ∣ (π‘€β€˜0) = 𝑣})
212, 3, 20cmpt 5192 . 2 class (𝑔 ∈ V ↦ (𝑣 ∈ (Vtxβ€˜π‘”), 𝑛 ∈ β„•0 ↦ {𝑀 ∈ (𝑛 ClWWalksN 𝑔) ∣ (π‘€β€˜0) = 𝑣}))
221, 21wceq 1542 1 wff ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtxβ€˜π‘”), 𝑛 ∈ β„•0 ↦ {𝑀 ∈ (𝑛 ClWWalksN 𝑔) ∣ (π‘€β€˜0) = 𝑣}))
Colors of variables: wff setvar class
This definition is referenced by:  clwwlknonmpo  29082
  Copyright terms: Public domain W3C validator