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

Definition df-clwwlksn 26762
Description: Define the set of all closed walks (in an undirected graph) of a fixed length n as words over the set of vertices. 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 26553. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
Assertion
Ref Expression
df-clwwlksn ClWWalksN = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (#‘𝑤) = 𝑛})
Distinct variable group:   𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-clwwlksn
StepHypRef Expression
1 cclwwlksn 26760 . 2 class ClWWalksN
2 vn . . 3 setvar 𝑛
3 vg . . 3 setvar 𝑔
4 cn 10972 . . 3 class
5 cvv 3189 . . 3 class V
6 vw . . . . . . 7 setvar 𝑤
76cv 1479 . . . . . 6 class 𝑤
8 chash 13065 . . . . . 6 class #
97, 8cfv 5852 . . . . 5 class (#‘𝑤)
102cv 1479 . . . . 5 class 𝑛
119, 10wceq 1480 . . . 4 wff (#‘𝑤) = 𝑛
123cv 1479 . . . . 5 class 𝑔
13 cclwwlks 26759 . . . . 5 class ClWWalks
1412, 13cfv 5852 . . . 4 class (ClWWalks‘𝑔)
1511, 6, 14crab 2911 . . 3 class {𝑤 ∈ (ClWWalks‘𝑔) ∣ (#‘𝑤) = 𝑛}
162, 3, 4, 5, 15cmpt2 6612 . 2 class (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (#‘𝑤) = 𝑛})
171, 16wceq 1480 1 wff ClWWalksN = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (#‘𝑤) = 𝑛})
Colors of variables: wff setvar class
This definition is referenced by:  clwwlksn  26765  clwwlknbp0  26768
  Copyright terms: Public domain W3C validator