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

Definition df-iedg 25777
 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 25775 . 2 class iEdg
2 vg . . 3 setvar 𝑔
3 cvv 3186 . . 3 class V
42cv 1479 . . . . 5 class 𝑔
53, 3cxp 5072 . . . . 5 class (V × V)
64, 5wcel 1987 . . . 4 wff 𝑔 ∈ (V × V)
7 c2nd 7112 . . . . 5 class 2nd
84, 7cfv 5847 . . . 4 class (2nd𝑔)
9 cedgf 25767 . . . . 5 class .ef
104, 9cfv 5847 . . . 4 class (.ef‘𝑔)
116, 8, 10cif 4058 . . 3 class if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔))
122, 3, 11cmpt 4673 . 2 class (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔)))
131, 12wceq 1480 1 wff iEdg = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd𝑔), (.ef‘𝑔)))
 Colors of variables: wff setvar class This definition is referenced by:  iedgval  25779  iedgvalOLD  25781
 Copyright terms: Public domain W3C validator