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 = ~P ( Pairs ` V )
	sprsymrelf.r	|- R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
	sprsymrelf.f	|- F = ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } )
Assertion	sprsymrelf1o	|- ( V e. W -> F : P -1-1-onto-> R )

Proof

Step	Hyp	Ref	Expression
1		sprsymrelf.p	|- P = ~P ( Pairs ` V )
2		sprsymrelf.r	|- R = { r e. ~P ( V X. V ) | A. x e. V A. y e. V ( x r y <-> y r x ) }
3		sprsymrelf.f	|- F = ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } )
4	1 2 3	sprsymrelf1	|- F : P -1-1-> R
5	4	a1i	|- ( V e. W -> F : P -1-1-> R )
6	1 2 3	sprsymrelfo	|- ( V e. 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 e. W -> F : P -1-1-onto-> R )