Theorem elpr2elpr

Description: For an element A of an unordered pair which is a subset of a given set V , there is another (maybe the same) element b of the given set V being an element of the unordered pair. (Contributed by AV, 5-Dec-2020)

	Ref	Expression
Assertion	elpr2elpr	$$⊢\left(X\in V\wedge Y\in V\wedge A\in \left\{X,Y\right\}\right)\to \exists b\in V\left\{X,Y\right\}=\left\{A,b\right\}$$

Proof

Step	Hyp	Ref	Expression
1		simprr	$$⊢\left(A=X\wedge \left(X\in V\wedge Y\in V\right)\right)\to Y\in V$$
2		preq2	$$⊢b=Y\to \left\{A,b\right\}=\left\{A,Y\right\}$$
3	2	eqeq2d	$$⊢b=Y\to \left(\left\{X,Y\right\}=\left\{A,b\right\}\leftrightarrow \left\{X,Y\right\}=\left\{A,Y\right\}\right)$$
4	3	adantl	$$⊢\left(\left(A=X\wedge \left(X\in V\wedge Y\in V\right)\right)\wedge b=Y\right)\to \left(\left\{X,Y\right\}=\left\{A,b\right\}\leftrightarrow \left\{X,Y\right\}=\left\{A,Y\right\}\right)$$
5		preq1	$$⊢X=A\to \left\{X,Y\right\}=\left\{A,Y\right\}$$
6	5	eqcoms	$$⊢A=X\to \left\{X,Y\right\}=\left\{A,Y\right\}$$
7	6	adantr	$$⊢\left(A=X\wedge \left(X\in V\wedge Y\in V\right)\right)\to \left\{X,Y\right\}=\left\{A,Y\right\}$$
8	1 4 7	rspcedvd	$$⊢\left(A=X\wedge \left(X\in V\wedge Y\in V\right)\right)\to \exists b\in V\left\{X,Y\right\}=\left\{A,b\right\}$$
9	8	ex	$$⊢A=X\to \left(\left(X\in V\wedge Y\in V\right)\to \exists b\in V\left\{X,Y\right\}=\left\{A,b\right\}\right)$$
10		simprl	$$⊢\left(A=Y\wedge \left(X\in V\wedge Y\in V\right)\right)\to X\in V$$
11		preq2	$$⊢b=X\to \left\{A,b\right\}=\left\{A,X\right\}$$
12	11	eqeq2d	$$⊢b=X\to \left(\left\{X,Y\right\}=\left\{A,b\right\}\leftrightarrow \left\{X,Y\right\}=\left\{A,X\right\}\right)$$
13	12	adantl	$$⊢\left(\left(A=Y\wedge \left(X\in V\wedge Y\in V\right)\right)\wedge b=X\right)\to \left(\left\{X,Y\right\}=\left\{A,b\right\}\leftrightarrow \left\{X,Y\right\}=\left\{A,X\right\}\right)$$
14		preq2	$$⊢Y=A\to \left\{X,Y\right\}=\left\{X,A\right\}$$
15	14	eqcoms	$$⊢A=Y\to \left\{X,Y\right\}=\left\{X,A\right\}$$
16		prcom	$$⊢\left\{X,A\right\}=\left\{A,X\right\}$$
17	15 16	syl6eq	$$⊢A=Y\to \left\{X,Y\right\}=\left\{A,X\right\}$$
18	17	adantr	$$⊢\left(A=Y\wedge \left(X\in V\wedge Y\in V\right)\right)\to \left\{X,Y\right\}=\left\{A,X\right\}$$
19	10 13 18	rspcedvd	$$⊢\left(A=Y\wedge \left(X\in V\wedge Y\in V\right)\right)\to \exists b\in V\left\{X,Y\right\}=\left\{A,b\right\}$$
20	19	ex	$$⊢A=Y\to \left(\left(X\in V\wedge Y\in V\right)\to \exists b\in V\left\{X,Y\right\}=\left\{A,b\right\}\right)$$
21	9 20	jaoi	$$⊢\left(A=X\vee A=Y\right)\to \left(\left(X\in V\wedge Y\in V\right)\to \exists b\in V\left\{X,Y\right\}=\left\{A,b\right\}\right)$$
22		elpri	$$⊢A\in \left\{X,Y\right\}\to \left(A=X\vee A=Y\right)$$
23	21 22	syl11	$$⊢\left(X\in V\wedge Y\in V\right)\to \left(A\in \left\{X,Y\right\}\to \exists b\in V\left\{X,Y\right\}=\left\{A,b\right\}\right)$$
24	23	3impia	$$⊢\left(X\in V\wedge Y\in V\wedge A\in \left\{X,Y\right\}\right)\to \exists b\in V\left\{X,Y\right\}=\left\{A,b\right\}$$