Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-wlks | Structured version Visualization version Unicode version |
Description: Define the set of all
walks (in a hypergraph). Such walks correspond to
the s-walks "on the vertex level" (with s = 1), and also to
1-walks "on
the edge level" (see wlk1walk 26535) discussed in Aksoy et al. The
predicate Walks can be read as "The
pair
represents a walk in a graph ", see also iswlk 26506.
The condition iEdg (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. should be allowed only if there is a loop at . Otherwise, C would be fulfilled by each edge containing . According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by AV, 30-Dec-2020.) |
Ref | Expression |
---|---|
df-wlks | Walks Word iEdg Vtx ..^if- iEdg iEdg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cwlks 26492 | . 2 Walks | |
2 | vg | . . 3 | |
3 | cvv 3200 | . . 3 | |
4 | vf | . . . . . . 7 | |
5 | 4 | cv 1482 | . . . . . 6 |
6 | 2 | cv 1482 | . . . . . . . . 9 |
7 | ciedg 25875 | . . . . . . . . 9 iEdg | |
8 | 6, 7 | cfv 5888 | . . . . . . . 8 iEdg |
9 | 8 | cdm 5114 | . . . . . . 7 iEdg |
10 | 9 | cword 13291 | . . . . . 6 Word iEdg |
11 | 5, 10 | wcel 1990 | . . . . 5 Word iEdg |
12 | cc0 9936 | . . . . . . 7 | |
13 | chash 13117 | . . . . . . . 8 | |
14 | 5, 13 | cfv 5888 | . . . . . . 7 |
15 | cfz 12326 | . . . . . . 7 | |
16 | 12, 14, 15 | co 6650 | . . . . . 6 |
17 | cvtx 25874 | . . . . . . 7 Vtx | |
18 | 6, 17 | cfv 5888 | . . . . . 6 Vtx |
19 | vp | . . . . . . 7 | |
20 | 19 | cv 1482 | . . . . . 6 |
21 | 16, 18, 20 | wf 5884 | . . . . 5 Vtx |
22 | vk | . . . . . . . . . 10 | |
23 | 22 | cv 1482 | . . . . . . . . 9 |
24 | 23, 20 | cfv 5888 | . . . . . . . 8 |
25 | c1 9937 | . . . . . . . . . 10 | |
26 | caddc 9939 | . . . . . . . . . 10 | |
27 | 23, 25, 26 | co 6650 | . . . . . . . . 9 |
28 | 27, 20 | cfv 5888 | . . . . . . . 8 |
29 | 24, 28 | wceq 1483 | . . . . . . 7 |
30 | 23, 5 | cfv 5888 | . . . . . . . . 9 |
31 | 30, 8 | cfv 5888 | . . . . . . . 8 iEdg |
32 | 24 | csn 4177 | . . . . . . . 8 |
33 | 31, 32 | wceq 1483 | . . . . . . 7 iEdg |
34 | 24, 28 | cpr 4179 | . . . . . . . 8 |
35 | 34, 31 | wss 3574 | . . . . . . 7 iEdg |
36 | 29, 33, 35 | wif 1012 | . . . . . 6 if- iEdg iEdg |
37 | cfzo 12465 | . . . . . . 7 ..^ | |
38 | 12, 14, 37 | co 6650 | . . . . . 6 ..^ |
39 | 36, 22, 38 | wral 2912 | . . . . 5 ..^if- iEdg iEdg |
40 | 11, 21, 39 | w3a 1037 | . . . 4 Word iEdg Vtx ..^if- iEdg iEdg |
41 | 40, 4, 19 | copab 4712 | . . 3 Word iEdg Vtx ..^if- iEdg iEdg |
42 | 2, 3, 41 | cmpt 4729 | . 2 Word iEdg Vtx ..^if- iEdg iEdg |
43 | 1, 42 | wceq 1483 | 1 Walks Word iEdg Vtx ..^if- iEdg iEdg |
Colors of variables: wff setvar class |
This definition is referenced by: wksfval 26505 relwlk 26521 |
Copyright terms: Public domain | W3C validator |