Metamath Proof Explorer

Theorem vtxval

Description: The set of vertices of a graph. (Contributed by AV, 9-Jan-2020) (Revised by AV, 21-Sep-2020)

Ref Expression
Assertion vtxval 
|- ( Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( g = G -> ( g e. ( _V X. _V ) <-> G e. ( _V X. _V ) ) )
2 fveq2 
 |-  ( g = G -> ( 1st ` g ) = ( 1st ` G ) )
3 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
4 1 2 3 ifbieq12d 
 |-  ( g = G -> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) )
5 df-vtx 
 |-  Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
6 fvex 
 |-  ( 1st ` G ) e. _V
7 fvex 
 |-  ( Base ` G ) e. _V
8 6 7 ifex 
 |-  if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) e. _V
9 4 5 8 fvmpt 
 |-  ( G e. _V -> ( Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) )
10 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
11 prcnel 
 |-  ( -. G e. _V -> -. G e. ( _V X. _V ) )
12 11 iffalsed 
 |-  ( -. G e. _V -> if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) = ( Base ` G ) )
13 fvprc 
 |-  ( -. G e. _V -> ( Vtx ` G ) = (/) )
14 10 12 13 3eqtr4rd 
 |-  ( -. G e. _V -> ( Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) )
15 9 14 pm2.61i 
 |-  ( Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) )