Metamath Proof Explorer

Theorem usgrsizedg

Description: In a simple graph, the size of the edge function is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020) (Revised by AV, 7-Jun-2021)

Ref Expression
Assertion usgrsizedg 
|- ( G e. USGraph -> ( # ` ( iEdg ` G ) ) = ( # ` ( Edg ` G ) ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( iEdg ` G ) e. _V
2 1 dmex 
 |-  dom ( iEdg ` G ) e. _V
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 3 4 usgrf 
 |-  ( G e. USGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } )
6 hashf1rn 
 |-  ( ( dom ( iEdg ` G ) e. _V /\ ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } ) -> ( # ` ( iEdg ` G ) ) = ( # ` ran ( iEdg ` G ) ) )
7 2 5 6 sylancr 
 |-  ( G e. USGraph -> ( # ` ( iEdg ` G ) ) = ( # ` ran ( iEdg ` G ) ) )
8 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
9 8 a1i 
 |-  ( G e. USGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
10 9 fveq2d 
 |-  ( G e. USGraph -> ( # ` ( Edg ` G ) ) = ( # ` ran ( iEdg ` G ) ) )
11 7 10 eqtr4d 
 |-  ( G e. USGraph -> ( # ` ( iEdg ` G ) ) = ( # ` ( Edg ` G ) ) )