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

Definition df-edg 25111
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.)
Assertion
Ref Expression
df-edg  |- Edges  =  ( g  e.  _V  |->  ran  ( 2nd `  g
) )

Detailed syntax breakdown of Definition df-edg
StepHypRef Expression
1 cedg 25106 . 2  class Edges
2 vg . . 3  setvar  g
3 cvv 3056 . . 3  class  _V
42cv 1453 . . . . 5  class  g
5 c2nd 6818 . . . . 5  class  2nd
64, 5cfv 5600 . . . 4  class  ( 2nd `  g )
76crn 4853 . . 3  class  ran  ( 2nd `  g )
82, 3, 7cmpt 4474 . 2  class  ( g  e.  _V  |->  ran  ( 2nd `  g ) )
91, 8wceq 1454 1  wff Edges  =  ( g  e.  _V  |->  ran  ( 2nd `  g
) )
Colors of variables: wff setvar class
This definition is referenced by:  edgval  25114
  Copyright terms: Public domain W3C validator