Metamath Proof Explorer


Theorem usgrfun

Description: The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017) (Revised by AV, 13-Oct-2020)

Ref Expression
Assertion usgrfun
|- ( G e. USGraph -> Fun ( iEdg ` G ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 usgrfs
 |-  ( G e. USGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
4 f1fun
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } -> Fun ( iEdg ` G ) )
5 3 4 syl
 |-  ( G e. USGraph -> Fun ( iEdg ` G ) )