Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-clwwlknon | Structured version Visualization version GIF version |
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 27712. 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.) |
Ref | Expression |
---|---|
df-clwwlknon | ⊢ ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cclwwlknon 28024 | . 2 class ClWWalksNOn | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3398 | . . 3 class V | |
4 | vv | . . . 4 setvar 𝑣 | |
5 | vn | . . . 4 setvar 𝑛 | |
6 | 2 | cv 1541 | . . . . 5 class 𝑔 |
7 | cvtx 26941 | . . . . 5 class Vtx | |
8 | 6, 7 | cfv 6339 | . . . 4 class (Vtx‘𝑔) |
9 | cn0 11976 | . . . 4 class ℕ0 | |
10 | cc0 10615 | . . . . . . 7 class 0 | |
11 | vw | . . . . . . . 8 setvar 𝑤 | |
12 | 11 | cv 1541 | . . . . . . 7 class 𝑤 |
13 | 10, 12 | cfv 6339 | . . . . . 6 class (𝑤‘0) |
14 | 4 | cv 1541 | . . . . . 6 class 𝑣 |
15 | 13, 14 | wceq 1542 | . . . . 5 wff (𝑤‘0) = 𝑣 |
16 | 5 | cv 1541 | . . . . . 6 class 𝑛 |
17 | cclwwlkn 27961 | . . . . . 6 class ClWWalksN | |
18 | 16, 6, 17 | co 7170 | . . . . 5 class (𝑛 ClWWalksN 𝑔) |
19 | 15, 11, 18 | crab 3057 | . . . 4 class {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣} |
20 | 4, 5, 8, 9, 19 | cmpo 7172 | . . 3 class (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}) |
21 | 2, 3, 20 | cmpt 5110 | . 2 class (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣})) |
22 | 1, 21 | wceq 1542 | 1 wff ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣})) |
Colors of variables: wff setvar class |
This definition is referenced by: clwwlknonmpo 28026 |
Copyright terms: Public domain | W3C validator |