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=𝒫\mathrm{Pairs}\left(V\right)$$
	sprsymrelf.r	$$⊢R=\left\{r\in 𝒫\left(V\times V\right)|\forall x\in V\forall y\in V\left(xry\leftrightarrow yrx\right)\right\}$$
	sprsymrelf.f	$$⊢F=\left(p\in P⟼\left\{⟨x,y⟩|\exists c\in pc=\left\{x,y\right\}\right\}\right)$$
Assertion	sprsymrelf1o	$$⊢V\in W\to F:P\underset{1-1\; onto}{⟶}R$$

Proof

Step	Hyp	Ref	Expression
1		sprsymrelf.p	$$⊢P=𝒫\mathrm{Pairs}\left(V\right)$$
2		sprsymrelf.r	$$⊢R=\left\{r\in 𝒫\left(V\times V\right)|\forall x\in V\forall y\in V\left(xry\leftrightarrow yrx\right)\right\}$$
3		sprsymrelf.f	$$⊢F=\left(p\in P⟼\left\{⟨x,y⟩|\exists c\in pc=\left\{x,y\right\}\right\}\right)$$
4	1 2 3	sprsymrelf1	$$⊢F:P\underset{1-1}{⟶}R$$
5	4	a1i	$$⊢V\in W\to F:P\underset{1-1}{⟶}R$$
6	1 2 3	sprsymrelfo	$$⊢V\in W\to F:P\underset{onto}{⟶}R$$
7		df-f1o	$$⊢F:P\underset{1-1\; onto}{⟶}R\leftrightarrow \left(F:P\underset{1-1}{⟶}R\wedge F:P\underset{onto}{⟶}R\right)$$
8	5 6 7	sylanbrc	$$⊢V\in W\to F:P\underset{1-1\; onto}{⟶}R$$