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

Definition df-clwwlkn 27171
Description: Define the set of all closed walks of a fixed length 𝑛 as words over the set of vertices in a graph 𝑔. If 0 < 𝑛, such a word corresponds to the sequence 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) as defined in df-clwlks 26899. For 𝑛 = 0, the set is empty, see clwwlkn0 27177. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
Assertion
Ref Expression
df-clwwlkn ClWWalksN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛})
Distinct variable group:   𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-clwwlkn
StepHypRef Expression
1 cclwwlkn 27169 . 2 class ClWWalksN
2 vn . . 3 setvar 𝑛
3 vg . . 3 setvar 𝑔
4 cn0 11505 . . 3 class 0
5 cvv 3341 . . 3 class V
6 vw . . . . . . 7 setvar 𝑤
76cv 1631 . . . . . 6 class 𝑤
8 chash 13332 . . . . . 6 class
97, 8cfv 6050 . . . . 5 class (♯‘𝑤)
102cv 1631 . . . . 5 class 𝑛
119, 10wceq 1632 . . . 4 wff (♯‘𝑤) = 𝑛
123cv 1631 . . . . 5 class 𝑔
13 cclwwlk 27126 . . . . 5 class ClWWalks
1412, 13cfv 6050 . . . 4 class (ClWWalks‘𝑔)
1511, 6, 14crab 3055 . . 3 class {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛}
162, 3, 4, 5, 15cmpt2 6817 . 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛})
171, 16wceq 1632 1 wff ClWWalksN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛})
Colors of variables: wff setvar class
This definition is referenced by:  clwwlkn  27173  clwwlkneq0  27178
  Copyright terms: Public domain W3C validator