Theorem isuhgrop

Description: The property of being an undirected hypergraph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of Bollobas p. 1. (Contributed by AV, 1-Jan-2020) (Revised by AV, 9-Oct-2020)

	Ref	Expression
Assertion	isuhgrop	|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		opex	|- <. V , E >. e. _V
2		eqid	|- ( Vtx ` <. V , E >. ) = ( Vtx ` <. V , E >. )
3		eqid	|- ( iEdg ` <. V , E >. ) = ( iEdg ` <. V , E >. )
4	2 3	isuhgr	|- ( <. V , E >. e. _V -> ( <. V , E >. e. UHGraph <-> ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) --> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) ) )
5	1 4	mp1i	|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. UHGraph <-> ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) --> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) ) )
6		opiedgfv	|- ( ( V e. W /\ E e. X ) -> ( iEdg ` <. V , E >. ) = E )
7	6	dmeqd	|- ( ( V e. W /\ E e. X ) -> dom ( iEdg ` <. V , E >. ) = dom E )
8		opvtxfv	|- ( ( V e. W /\ E e. X ) -> ( Vtx ` <. V , E >. ) = V )
9	8	pweqd	|- ( ( V e. W /\ E e. X ) -> ~P ( Vtx ` <. V , E >. ) = ~P V )
10	9	difeq1d	|- ( ( V e. W /\ E e. X ) -> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) = ( ~P V \ { (/) } ) )
11	6 7 10	feq123d	|- ( ( V e. W /\ E e. X ) -> ( ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) --> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) <-> E : dom E --> ( ~P V \ { (/) } ) ) )
12	5 11	bitrd	|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) )