Metamath Proof Explorer


Theorem sprsymrelen

Description: The class P of subsets of the set of pairs over a fixed set V and the class R of symmetric relations on the fixed set V are equinumerous. (Contributed by AV, 27-Nov-2021)

Ref Expression
Hypotheses sprsymrelf.p P = 𝒫 Pairs V
sprsymrelf.r R = r 𝒫 V × V | x V y V x r y y r x
Assertion sprsymrelen V W P R

Proof

Step Hyp Ref Expression
1 sprsymrelf.p P = 𝒫 Pairs V
2 sprsymrelf.r R = r 𝒫 V × V | x V y V x r y y r x
3 1 2 sprbisymrel V W f f : P 1-1 onto R
4 bren P R f f : P 1-1 onto R
5 3 4 sylibr V W P R