Metamath Proof Explorer


Theorem uspgrushgr

Description: A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020) (Revised by AV, 15-Oct-2020)

Ref Expression
Assertion uspgrushgr G USHGraph G USHGraph

Proof

Step Hyp Ref Expression
1 eqid Vtx G = Vtx G
2 eqid iEdg G = iEdg G
3 1 2 isuspgr G USHGraph G USHGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2
4 ssrab2 x 𝒫 Vtx G | x 2 𝒫 Vtx G
5 f1ss iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2 x 𝒫 Vtx G | x 2 𝒫 Vtx G iEdg G : dom iEdg G 1-1 𝒫 Vtx G
6 4 5 mpan2 iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2 iEdg G : dom iEdg G 1-1 𝒫 Vtx G
7 3 6 syl6bi G USHGraph G USHGraph iEdg G : dom iEdg G 1-1 𝒫 Vtx G
8 1 2 isushgr G USHGraph G USHGraph iEdg G : dom iEdg G 1-1 𝒫 Vtx G
9 7 8 sylibrd G USHGraph G USHGraph G USHGraph
10 9 pm2.43i G USHGraph G USHGraph