Metamath Proof Explorer


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 \ { (/) } ) ) )