Theorem sprsymrelfv

Description: The value of the function F which maps a subset of the set of pairs over a fixed set V to the relation relating two elements of the set V iff they are in a pair of the subset. (Contributed by AV, 19-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	sprsymrelfv	|- ( X e. P -> ( F ` X ) = { <. x , y >. | E. c e. X c = { x , y } } )

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		rexeq	|- ( p = X -> ( E. c e. p c = { x , y } <-> E. c e. X c = { x , y } ) )
5	4	opabbidv	|- ( p = X -> { <. x , y >. | E. c e. p c = { x , y } } = { <. x , y >. | E. c e. X c = { x , y } } )
6		id	|- ( X e. P -> X e. P )
7		elpwi	|- ( X e. ~P ( Pairs ` V ) -> X C_ ( Pairs ` V ) )
8	7 1	eleq2s	|- ( X e. P -> X C_ ( Pairs ` V ) )
9		sprsymrelfvlem	|- ( X C_ ( Pairs ` V ) -> { <. x , y >. | E. c e. X c = { x , y } } e. ~P ( V X. V ) )
10	8 9	syl	|- ( X e. P -> { <. x , y >. | E. c e. X c = { x , y } } e. ~P ( V X. V ) )
11	3 5 6 10	fvmptd3	|- ( X e. P -> ( F ` X ) = { <. x , y >. | E. c e. X c = { x , y } } )