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 29018
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 28768. For 𝑛 = 0, the set is empty, see clwwlkn0 29021. (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 29017 . 2 class ClWWalksN
2 vn . . 3 setvar 𝑛
3 vg . . 3 setvar 𝑔
4 cn0 12421 . . 3 class β„•0
5 cvv 3447 . . 3 class V
6 vw . . . . . . 7 setvar 𝑀
76cv 1541 . . . . . 6 class 𝑀
8 chash 14239 . . . . . 6 class β™―
97, 8cfv 6500 . . . . 5 class (β™―β€˜π‘€)
102cv 1541 . . . . 5 class 𝑛
119, 10wceq 1542 . . . 4 wff (β™―β€˜π‘€) = 𝑛
123cv 1541 . . . . 5 class 𝑔
13 cclwwlk 28974 . . . . 5 class ClWWalks
1412, 13cfv 6500 . . . 4 class (ClWWalksβ€˜π‘”)
1511, 6, 14crab 3406 . . 3 class {𝑀 ∈ (ClWWalksβ€˜π‘”) ∣ (β™―β€˜π‘€) = 𝑛}
162, 3, 4, 5, 15cmpo 7363 . 2 class (𝑛 ∈ β„•0, 𝑔 ∈ V ↦ {𝑀 ∈ (ClWWalksβ€˜π‘”) ∣ (β™―β€˜π‘€) = 𝑛})
171, 16wceq 1542 1 wff ClWWalksN = (𝑛 ∈ β„•0, 𝑔 ∈ V ↦ {𝑀 ∈ (ClWWalksβ€˜π‘”) ∣ (β™―β€˜π‘€) = 𝑛})
Colors of variables: wff setvar class
This definition is referenced by:  clwwlkn  29019  clwwlkneq0  29022
  Copyright terms: Public domain W3C validator