Metamath Proof Explorer

Theorem iedgval

Description: The set of indexed edges of a graph. (Contributed by AV, 21-Sep-2020)

Ref Expression
Assertion iedgval 
|- ( iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) )

Proof

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