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 )