This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ushgruhgr

Description: An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020) (Revised by AV, 9-Oct-2020)

Ref Expression
Assertion ushgruhgr 
|- ( G e. USHGraph -> G e. UHGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 ushgrf 
 |-  ( G e. USHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) )
4 f1f 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) )
5 3 4 syl 
 |-  ( G e. USHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) )
6 1 2 isuhgr 
 |-  ( G e. USHGraph -> ( G e. UHGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
7 5 6 mpbird 
 |-  ( G e. USHGraph -> G e. UHGraph )