Theorem elsprel

Description: An unordered pair is an element of all unordered pairs. At least one of the two elements of the unordered pair must be a set. Otherwise, the unordered pair would be the empty set, see prprc , which is not an element of all unordered pairs, see spr0nelg . (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	elsprel	$$⊢\left(A\in V\vee B\in W\right)\to \left\{A,B\right\}\in \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		elex	$$⊢B\in W\to B\in \mathrm{V}$$
3	1 2	orim12i	$$⊢\left(A\in V\vee B\in W\right)\to \left(A\in \mathrm{V}\vee B\in \mathrm{V}\right)$$
4		elisset	$$⊢A\in \mathrm{V}\to \exists aa=A$$
5		elisset	$$⊢B\in \mathrm{V}\to \exists bb=B$$
6		exdistrv	$$⊢\exists a\exists b\left(a=A\wedge b=B\right)\leftrightarrow \left(\exists aa=A\wedge \exists bb=B\right)$$
7		preq12	$$⊢\left(a=A\wedge b=B\right)\to \left\{a,b\right\}=\left\{A,B\right\}$$
8	7	eqcomd	$$⊢\left(a=A\wedge b=B\right)\to \left\{A,B\right\}=\left\{a,b\right\}$$
9	8	2eximi	$$⊢\exists a\exists b\left(a=A\wedge b=B\right)\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
10	6 9	sylbir	$$⊢\left(\exists aa=A\wedge \exists bb=B\right)\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
11	4 5 10	syl2an	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
12	11	expcom	$$⊢B\in \mathrm{V}\to \left(A\in \mathrm{V}\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}\right)$$
13		preq2	$$⊢b=a\to \left\{a,b\right\}=\left\{a,a\right\}$$
14	13	adantr	$$⊢\left(b=a\wedge a=A\right)\to \left\{a,b\right\}=\left\{a,a\right\}$$
15		dfsn2	$$⊢\left\{a\right\}=\left\{a,a\right\}$$
16		sneq	$$⊢a=A\to \left\{a\right\}=\left\{A\right\}$$
17	16	adantl	$$⊢\left(b=a\wedge a=A\right)\to \left\{a\right\}=\left\{A\right\}$$
18	15 17	eqtr3id	$$⊢\left(b=a\wedge a=A\right)\to \left\{a,a\right\}=\left\{A\right\}$$
19	14 18	eqtr2d	$$⊢\left(b=a\wedge a=A\right)\to \left\{A\right\}=\left\{a,b\right\}$$
20	19	ex	$$⊢b=a\to \left(a=A\to \left\{A\right\}=\left\{a,b\right\}\right)$$
21	20	spimevw	$$⊢a=A\to \exists b\left\{A\right\}=\left\{a,b\right\}$$
22	21	adantl	$$⊢\left(\neg B\in \mathrm{V}\wedge a=A\right)\to \exists b\left\{A\right\}=\left\{a,b\right\}$$
23		prprc2	$$⊢\neg B\in \mathrm{V}\to \left\{A,B\right\}=\left\{A\right\}$$
24	23	adantr	$$⊢\left(\neg B\in \mathrm{V}\wedge a=A\right)\to \left\{A,B\right\}=\left\{A\right\}$$
25	24	eqeq1d	$$⊢\left(\neg B\in \mathrm{V}\wedge a=A\right)\to \left(\left\{A,B\right\}=\left\{a,b\right\}\leftrightarrow \left\{A\right\}=\left\{a,b\right\}\right)$$
26	25	exbidv	$$⊢\left(\neg B\in \mathrm{V}\wedge a=A\right)\to \left(\exists b\left\{A,B\right\}=\left\{a,b\right\}\leftrightarrow \exists b\left\{A\right\}=\left\{a,b\right\}\right)$$
27	22 26	mpbird	$$⊢\left(\neg B\in \mathrm{V}\wedge a=A\right)\to \exists b\left\{A,B\right\}=\left\{a,b\right\}$$
28	27	ex	$$⊢\neg B\in \mathrm{V}\to \left(a=A\to \exists b\left\{A,B\right\}=\left\{a,b\right\}\right)$$
29	28	eximdv	$$⊢\neg B\in \mathrm{V}\to \left(\exists aa=A\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}\right)$$
30	4 29	syl5	$$⊢\neg B\in \mathrm{V}\to \left(A\in \mathrm{V}\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}\right)$$
31	12 30	pm2.61i	$$⊢A\in \mathrm{V}\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
32	11	ex	$$⊢A\in \mathrm{V}\to \left(B\in \mathrm{V}\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}\right)$$
33		preq1	$$⊢a=b\to \left\{a,b\right\}=\left\{b,b\right\}$$
34	33	adantr	$$⊢\left(a=b\wedge b=B\right)\to \left\{a,b\right\}=\left\{b,b\right\}$$
35		dfsn2	$$⊢\left\{b\right\}=\left\{b,b\right\}$$
36		sneq	$$⊢b=B\to \left\{b\right\}=\left\{B\right\}$$
37	36	adantl	$$⊢\left(a=b\wedge b=B\right)\to \left\{b\right\}=\left\{B\right\}$$
38	35 37	eqtr3id	$$⊢\left(a=b\wedge b=B\right)\to \left\{b,b\right\}=\left\{B\right\}$$
39	34 38	eqtr2d	$$⊢\left(a=b\wedge b=B\right)\to \left\{B\right\}=\left\{a,b\right\}$$
40	39	ex	$$⊢a=b\to \left(b=B\to \left\{B\right\}=\left\{a,b\right\}\right)$$
41	40	spimevw	$$⊢b=B\to \exists a\left\{B\right\}=\left\{a,b\right\}$$
42	41	adantl	$$⊢\left(\neg A\in \mathrm{V}\wedge b=B\right)\to \exists a\left\{B\right\}=\left\{a,b\right\}$$
43		prprc1	$$⊢\neg A\in \mathrm{V}\to \left\{A,B\right\}=\left\{B\right\}$$
44	43	adantr	$$⊢\left(\neg A\in \mathrm{V}\wedge b=B\right)\to \left\{A,B\right\}=\left\{B\right\}$$
45	44	eqeq1d	$$⊢\left(\neg A\in \mathrm{V}\wedge b=B\right)\to \left(\left\{A,B\right\}=\left\{a,b\right\}\leftrightarrow \left\{B\right\}=\left\{a,b\right\}\right)$$
46	45	exbidv	$$⊢\left(\neg A\in \mathrm{V}\wedge b=B\right)\to \left(\exists a\left\{A,B\right\}=\left\{a,b\right\}\leftrightarrow \exists a\left\{B\right\}=\left\{a,b\right\}\right)$$
47	42 46	mpbird	$$⊢\left(\neg A\in \mathrm{V}\wedge b=B\right)\to \exists a\left\{A,B\right\}=\left\{a,b\right\}$$
48	47	ex	$$⊢\neg A\in \mathrm{V}\to \left(b=B\to \exists a\left\{A,B\right\}=\left\{a,b\right\}\right)$$
49	48	eximdv	$$⊢\neg A\in \mathrm{V}\to \left(\exists bb=B\to \exists b\exists a\left\{A,B\right\}=\left\{a,b\right\}\right)$$
50	49	impcom	$$⊢\left(\exists bb=B\wedge \neg A\in \mathrm{V}\right)\to \exists b\exists a\left\{A,B\right\}=\left\{a,b\right\}$$
51		excom	$$⊢\exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}\leftrightarrow \exists b\exists a\left\{A,B\right\}=\left\{a,b\right\}$$
52	50 51	sylibr	$$⊢\left(\exists bb=B\wedge \neg A\in \mathrm{V}\right)\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
53	52	ex	$$⊢\exists bb=B\to \left(\neg A\in \mathrm{V}\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}\right)$$
54	53 5	syl11	$$⊢\neg A\in \mathrm{V}\to \left(B\in \mathrm{V}\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}\right)$$
55	32 54	pm2.61i	$$⊢B\in \mathrm{V}\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
56	31 55	jaoi	$$⊢\left(A\in \mathrm{V}\vee B\in \mathrm{V}\right)\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
57	3 56	syl	$$⊢\left(A\in V\vee B\in W\right)\to \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
58		prex	$$⊢\left\{A,B\right\}\in \mathrm{V}$$
59		eqeq1	$$⊢p=\left\{A,B\right\}\to \left(p=\left\{a,b\right\}\leftrightarrow \left\{A,B\right\}=\left\{a,b\right\}\right)$$
60	59	2exbidv	$$⊢p=\left\{A,B\right\}\to \left(\exists a\exists bp=\left\{a,b\right\}\leftrightarrow \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}\right)$$
61	58 60	elab	$$⊢\left\{A,B\right\}\in \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}\leftrightarrow \exists a\exists b\left\{A,B\right\}=\left\{a,b\right\}$$
62	57 61	sylibr	$$⊢\left(A\in V\vee B\in W\right)\to \left\{A,B\right\}\in \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}$$