Definition df-vtx 16135

Description: Define the function mapping a graph to the set of its vertices. This definition is very general: It defines the set of vertices for any ordered pair as its first component, and for any other class as its "base set". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure representing a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 20-Sep-2020.)

Assertion

Ref	Expression
df-vtx	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )

Detailed syntax breakdown of Definition df-vtx

Step	Hyp	Ref	Expression
1		cvtx 16133	. 2 class Vtx
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		c1st 6345	. . . . 5 class 1st
8	4, 7	cfv 5357	. . . 4 class ( 1st ` g )
9		cbs 13296	. . . . 5 class Base
10	4, 9	cfv 5357	. . . 4 class ( Base ` g )
11	6, 8, 10	cif 3624	. . 3 class if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) )
12	2, 3, 11	cmpt 4176	. 2 class ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
13	1, 12	wceq 1398	1 wff Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )

This definition is referenced by:  vtxvalg  16137  1vgrex  16141  wlkreslem  16499  clwwlknonmpo  16549  trlsegvdegfi  16588  eupth2lem3lem1fi  16589  eupth2lem3lem2fi  16590  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594