Metamath Proof Explorer


Theorem uspgrspren

Description: The set G of the "simple pseudographs" with a fixed set of vertices V and the class P of subsets of the set of pairs over the fixed set V are equinumerous. (Contributed by AV, 27-Nov-2021)

Ref Expression
Hypotheses uspgrsprf.p P = 𝒫 Pairs V
uspgrsprf.g G = v e | v = V q USHGraph Vtx q = v Edg q = e
Assertion uspgrspren V W G P

Proof

Step Hyp Ref Expression
1 uspgrsprf.p P = 𝒫 Pairs V
2 uspgrsprf.g G = v e | v = V q USHGraph Vtx q = v Edg q = e
3 1 2 uspgrbispr V W f f : G 1-1 onto P
4 bren G P f f : G 1-1 onto P
5 3 4 sylibr V W G P