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

Definition df-edg 26110
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 of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless (e.g., edguhgr 26194). Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.)
Assertion
Ref Expression
df-edg Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))

Detailed syntax breakdown of Definition df-edg
StepHypRef Expression
1 cedg 26109 . 2 class Edg
2 vg . . 3 setvar 𝑔
3 cvv 3328 . . 3 class V
42cv 1619 . . . . 5 class 𝑔
5 ciedg 26045 . . . . 5 class iEdg
64, 5cfv 6037 . . . 4 class (iEdg‘𝑔)
76crn 5255 . . 3 class ran (iEdg‘𝑔)
82, 3, 7cmpt 4869 . 2 class (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
91, 8wceq 1620 1 wff Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
Colors of variables: wff setvar class
This definition is referenced by:  edgval  26111  edgvalOLD  26112
  Copyright terms: Public domain W3C validator