Metamath Proof Explorer

Theorem usgrumgr

Description: A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020)

Ref Expression
Assertion usgrumgr 
|- ( G e. USGraph -> G e. UMGraph )

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 f1f 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
5 3 4 syl 
 |-  ( G e. USGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
6 1 2 isumgrs 
 |-  ( G e. USGraph -> ( G e. UMGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
7 5 6 mpbird 
 |-  ( G e. USGraph -> G e. UMGraph )