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 = ~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 ) }
Assertion	sprbisymrel	|- ( V e. W -> E. f 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		fvex	|- ( Pairs ` V ) e. _V
4	3	pwex	|- ~P ( Pairs ` V ) e. _V
5	1 4	eqeltri	|- P e. _V
6		mptexg	|- ( P e. _V -> ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } ) e. _V )
7	5 6	mp1i	|- ( V e. W -> ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } ) e. _V )
8		eqid	|- ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } ) = ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } )
9	1 2 8	sprsymrelf1o	|- ( V e. W -> ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } ) : P -1-1-onto-> R )
10		f1oeq1	|- ( f = ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } ) -> ( f : P -1-1-onto-> R <-> ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } ) : P -1-1-onto-> R ) )
11	10	spcegv	|- ( ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } ) e. _V -> ( ( p e. P |-> { <. x , y >. | E. c e. p c = { x , y } } ) : P -1-1-onto-> R -> E. f f : P -1-1-onto-> R ) )
12	7 9 11	sylc	|- ( V e. W -> E. f f : P -1-1-onto-> R )