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

Definition df-iedg 26098
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 26096 . 2 class iEdg
2 vg . . 3 setvar 𝑔
3 cvv 3351 . . 3 class V
42cv 1630 . . . . 5 class 𝑔
53, 3cxp 5248 . . . . 5 class (V × V)
64, 5wcel 2145 . . . 4 wff 𝑔 ∈ (V × V)
7 c2nd 7318 . . . . 5 class 2nd
84, 7cfv 6030 . . . 4 class (2nd𝑔)
9 cedgf 26088 . . . . 5 class .ef
104, 9cfv 6030 . . . 4 class (.ef‘𝑔)
116, 8, 10cif 4226 . . 3 class if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔))
122, 3, 11cmpt 4864 . 2 class (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔)))
131, 12wceq 1631 1 wff iEdg = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔)))
Colors of variables: wff setvar class
This definition is referenced by:  iedgval  26100  iedgvalOLD  26102
  Copyright terms: Public domain W3C validator