Metamath Proof Explorer


Theorem upgruhgr

Description: An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 10-Oct-2020)

Ref Expression
Assertion upgruhgr GUPGraphGUHGraph

Proof

Step Hyp Ref Expression
1 eqid VtxG=VtxG
2 eqid iEdgG=iEdgG
3 1 2 upgrf GUPGraphiEdgG:domiEdgGx𝒫VtxG|x2
4 ssrab2 x𝒫VtxG|x2𝒫VtxG
5 fss iEdgG:domiEdgGx𝒫VtxG|x2x𝒫VtxG|x2𝒫VtxGiEdgG:domiEdgG𝒫VtxG
6 3 4 5 sylancl GUPGraphiEdgG:domiEdgG𝒫VtxG
7 1 2 isuhgr GUPGraphGUHGraphiEdgG:domiEdgG𝒫VtxG
8 6 7 mpbird GUPGraphGUHGraph