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 W E X V E UHGraph E : dom E 𝒫 V

Proof

Step Hyp Ref Expression
1 opex V E V
2 eqid Vtx V E = Vtx V E
3 eqid iEdg V E = iEdg V E
4 2 3 isuhgr V E V V E UHGraph iEdg V E : dom iEdg V E 𝒫 Vtx V E
5 1 4 mp1i V W E X V E UHGraph iEdg V E : dom iEdg V E 𝒫 Vtx V E
6 opiedgfv V W E X iEdg V E = E
7 6 dmeqd V W E X dom iEdg V E = dom E
8 opvtxfv V W E X Vtx V E = V
9 8 pweqd V W E X 𝒫 Vtx V E = 𝒫 V
10 9 difeq1d V W E X 𝒫 Vtx V E = 𝒫 V
11 6 7 10 feq123d V W E X iEdg V E : dom iEdg V E 𝒫 Vtx V E E : dom E 𝒫 V
12 5 11 bitrd V W E X V E UHGraph E : dom E 𝒫 V