Metamath Proof Explorer

Theorem edgval

Description: The edges of a graph. (Contributed by AV, 1-Jan-2020) (Revised by AV, 13-Oct-2020) (Revised by AV, 8-Dec-2021)

Ref Expression
Assertion edgval 
|- ( Edg ` G ) = ran ( iEdg ` G )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) )
2 1 rneqd 
 |-  ( g = G -> ran ( iEdg ` g ) = ran ( iEdg ` G ) )
3 df-edg 
 |-  Edg = ( g e. _V |-> ran ( iEdg ` g ) )
4 fvex 
 |-  ( iEdg ` G ) e. _V
5 4 rnex 
 |-  ran ( iEdg ` G ) e. _V
6 2 3 5 fvmpt 
 |-  ( G e. _V -> ( Edg ` G ) = ran ( iEdg ` G ) )
7 rn0 
 |-  ran (/) = (/)
8 7 a1i 
 |-  ( -. G e. _V -> ran (/) = (/) )
9 fvprc 
 |-  ( -. G e. _V -> ( iEdg ` G ) = (/) )
10 9 rneqd 
 |-  ( -. G e. _V -> ran ( iEdg ` G ) = ran (/) )
11 fvprc 
 |-  ( -. G e. _V -> ( Edg ` G ) = (/) )
12 8 10 11 3eqtr4rd 
 |-  ( -. G e. _V -> ( Edg ` G ) = ran ( iEdg ` G ) )
13 6 12 pm2.61i 
 |-  ( Edg ` G ) = ran ( iEdg ` G )