Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-edg | Structured version Visualization version GIF version |
Description: Define the class of edges of a graph, see also definition ("E = E(G)") in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges for any ordered pairs as the range of its second component (which even needs not to be a function). Therefore, this definition could also be used for hypergraphs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. Therefore, this definition should only be used for undirected simple graphs. (Contributed by AV, 1-Jan-2020.) |
Ref | Expression |
---|---|
df-edg | ⊢ Edges = (𝑔 ∈ V ↦ ran (2nd ‘𝑔)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cedg 25860 | . 2 class Edges | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3173 | . . 3 class V | |
4 | 2 | cv 1474 | . . . . 5 class 𝑔 |
5 | c2nd 7058 | . . . . 5 class 2nd | |
6 | 4, 5 | cfv 5804 | . . . 4 class (2nd ‘𝑔) |
7 | 6 | crn 5039 | . . 3 class ran (2nd ‘𝑔) |
8 | 2, 3, 7 | cmpt 4643 | . 2 class (𝑔 ∈ V ↦ ran (2nd ‘𝑔)) |
9 | 1, 8 | wceq 1475 | 1 wff Edges = (𝑔 ∈ V ↦ ran (2nd ‘𝑔)) |
Colors of variables: wff setvar class |
This definition is referenced by: edgval 25868 |
Copyright terms: Public domain | W3C validator |