Definition df-iedg 16136

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 = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )

Detailed syntax breakdown of Definition df-iedg

Step	Hyp	Ref	Expression
1		ciedg 16134	. 2 class iEdg
2		vg	. . 3 setvar g
3		cvv 2815	. . 3 class _V
4	2	cv 1397	. . . . 5 class g
5	3, 3	cxp 4752	. . . . 5 class ( _V X. _V )
6	4, 5	wcel 2205	. . . 4 wff g e. ( _V X. _V )
7		c2nd 6346	. . . . 5 class 2nd
8	4, 7	cfv 5357	. . . 4 class ( 2nd ` g )
9		cedgf 16125	. . . . 5 class .ef
10	4, 9	cfv 5357	. . . 4 class (.ef ` g )
11	6, 8, 10	cif 3624	. . 3 class if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) )
12	2, 3, 11	cmpt 4176	. 2 class ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
13	1, 12	wceq 1398	1 wff iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )

This definition is referenced by:  iedgvalg  16138  edgval  16181