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=𝒫\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	sprsymrelfv	$$⊢X\in P\to F\left(X\right)=\left\{⟨x,y⟩|\exists c\in Xc=\left\{x,y\right\}\right\}$$

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		rexeq	$$⊢p=X\to \left(\exists c\in pc=\left\{x,y\right\}\leftrightarrow \exists c\in Xc=\left\{x,y\right\}\right)$$
5	4	opabbidv	$$⊢p=X\to \left\{⟨x,y⟩|\exists c\in pc=\left\{x,y\right\}\right\}=\left\{⟨x,y⟩|\exists c\in Xc=\left\{x,y\right\}\right\}$$
6		id	$$⊢X\in P\to X\in P$$
7		elpwi	$$⊢X\in 𝒫\mathrm{Pairs}\left(V\right)\to X\subseteq \mathrm{Pairs}\left(V\right)$$
8	7 1	eleq2s	$$⊢X\in P\to X\subseteq \mathrm{Pairs}\left(V\right)$$
9		sprsymrelfvlem	$$⊢X\subseteq \mathrm{Pairs}\left(V\right)\to \left\{⟨x,y⟩|\exists c\in Xc=\left\{x,y\right\}\right\}\in 𝒫\left(V\times V\right)$$
10	8 9	syl	$$⊢X\in P\to \left\{⟨x,y⟩|\exists c\in Xc=\left\{x,y\right\}\right\}\in 𝒫\left(V\times V\right)$$
11	3 5 6 10	fvmptd3	$$⊢X\in P\to F\left(X\right)=\left\{⟨x,y⟩|\exists c\in Xc=\left\{x,y\right\}\right\}$$