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

Definition df-iedg 25676
 Description: Define the function mapping a graph to its indexed edges. This definition is very general: It defines the indexed edges for any ordered pair as its second component, and for any other class as its "edge function". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure (containing a slot for "edge functions") representing a graph. (Contributed by AV, 20-Sep-2020.)
Assertion
Ref Expression
df-iedg iEdg = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔)))

Detailed syntax breakdown of Definition df-iedg
StepHypRef Expression
1 ciedg 25674 . 2 class iEdg
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
42cv 1474 . . . . 5 class 𝑔
53, 3cxp 5036 . . . . 5 class (V × V)
64, 5wcel 1977 . . . 4 wff 𝑔 ∈ (V × V)
7 c2nd 7058 . . . . 5 class 2nd
84, 7cfv 5804 . . . 4 class (2nd𝑔)
9 cedgf 25667 . . . . 5 class .ef
104, 9cfv 5804 . . . 4 class (.ef‘𝑔)
116, 8, 10cif 4036 . . 3 class if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔))
122, 3, 11cmpt 4643 . 2 class (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔)))
131, 12wceq 1475 1 wff iEdg = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔)))
 Colors of variables: wff setvar class This definition is referenced by:  iedgval  25678
 Copyright terms: Public domain W3C validator