Metamath Proof Explorer


Theorem isuspgrop

Description: The property of being an undirected simple pseudograph 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, 25-Nov-2021)

Ref Expression
Assertion isuspgrop V W E X V E USHGraph E : dom E 1-1 p 𝒫 V | p 2

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 isuspgr V E V V E USHGraph iEdg V E : dom iEdg V E 1-1 p 𝒫 Vtx V E | p 2
5 1 4 mp1i V W E X V E USHGraph iEdg V E : dom iEdg V E 1-1 p 𝒫 Vtx V E | p 2
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 10 rabeqdv V W E X p 𝒫 Vtx V E | p 2 = p 𝒫 V | p 2
12 6 7 11 f1eq123d V W E X iEdg V E : dom iEdg V E 1-1 p 𝒫 Vtx V E | p 2 E : dom E 1-1 p 𝒫 V | p 2
13 5 12 bitrd V W E X V E USHGraph E : dom E 1-1 p 𝒫 V | p 2