Metamath Proof Explorer


Theorem sprbisymrel

Description: There is a bijection between the subsets of the set of pairs over a fixed set V and the symmetric relations R on the fixed set V . (Contributed by AV, 23-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 sprbisymrel V W f f : P 1-1 onto 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 fvex Pairs V V
4 3 pwex 𝒫 Pairs V V
5 1 4 eqeltri P V
6 mptexg P V p P x y | c p c = x y V
7 5 6 mp1i V W p P x y | c p c = x y V
8 eqid p P x y | c p c = x y = p P x y | c p c = x y
9 1 2 8 sprsymrelf1o V W p P x y | c p c = x y : P 1-1 onto R
10 f1oeq1 f = p P x y | c p c = x y f : P 1-1 onto R p P x y | c p c = x y : P 1-1 onto R
11 10 spcegv p P x y | c p c = x y V p P x y | c p c = x y : P 1-1 onto R f f : P 1-1 onto R
12 7 9 11 sylc V W f f : P 1-1 onto R