Metamath Proof Explorer


Theorem sprsymrelf1o

Description: The mapping F is a bijection between the subsets of the set of pairs over a fixed set V into 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
sprsymrelf.f F = p P x y | c p c = x y
Assertion sprsymrelf1o V W 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 sprsymrelf.f F = p P x y | c p c = x y
4 1 2 3 sprsymrelf1 F : P 1-1 R
5 4 a1i V W F : P 1-1 R
6 1 2 3 sprsymrelfo V W F : P onto R
7 df-f1o F : P 1-1 onto R F : P 1-1 R F : P onto R
8 5 6 7 sylanbrc V W F : P 1-1 onto R