Theorem pr2ne

Description: If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010)

	Ref	Expression
Assertion	pr2ne	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A,B\right\}\approx 2_{𝑜}\leftrightarrow A\ne B\right)$$

Proof

Step	Hyp	Ref	Expression
1		preq2	$$⊢B=A\to \left\{A,B\right\}=\left\{A,A\right\}$$
2	1	eqcoms	$$⊢A=B\to \left\{A,B\right\}=\left\{A,A\right\}$$
3		enpr1g	$$⊢A\in C\to \left\{A,A\right\}\approx 1_{𝑜}$$
4		entr	$$⊢\left(\left\{A,B\right\}\approx \left\{A,A\right\}\wedge \left\{A,A\right\}\approx 1_{𝑜}\right)\to \left\{A,B\right\}\approx 1_{𝑜}$$
5		1sdom2	$$⊢1_{𝑜}\prec 2_{𝑜}$$
6		sdomnen	$$⊢1_{𝑜}\prec 2_{𝑜}\to \neg 1_{𝑜}\approx 2_{𝑜}$$
7	5 6	ax-mp	$$⊢\neg 1_{𝑜}\approx 2_{𝑜}$$
8		ensym	$$⊢\left\{A,B\right\}\approx 1_{𝑜}\to 1_{𝑜}\approx \left\{A,B\right\}$$
9		entr	$$⊢\left(1_{𝑜}\approx \left\{A,B\right\}\wedge \left\{A,B\right\}\approx 2_{𝑜}\right)\to 1_{𝑜}\approx 2_{𝑜}$$
10	9	ex	$$⊢1_{𝑜}\approx \left\{A,B\right\}\to \left(\left\{A,B\right\}\approx 2_{𝑜}\to 1_{𝑜}\approx 2_{𝑜}\right)$$
11	8 10	syl	$$⊢\left\{A,B\right\}\approx 1_{𝑜}\to \left(\left\{A,B\right\}\approx 2_{𝑜}\to 1_{𝑜}\approx 2_{𝑜}\right)$$
12	7 11	mtoi	$$⊢\left\{A,B\right\}\approx 1_{𝑜}\to \neg \left\{A,B\right\}\approx 2_{𝑜}$$
13	12	a1d	$$⊢\left\{A,B\right\}\approx 1_{𝑜}\to \left(\left(A\in C\wedge B\in D\right)\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)$$
14	4 13	syl	$$⊢\left(\left\{A,B\right\}\approx \left\{A,A\right\}\wedge \left\{A,A\right\}\approx 1_{𝑜}\right)\to \left(\left(A\in C\wedge B\in D\right)\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)$$
15	14	ex	$$⊢\left\{A,B\right\}\approx \left\{A,A\right\}\to \left(\left\{A,A\right\}\approx 1_{𝑜}\to \left(\left(A\in C\wedge B\in D\right)\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)\right)$$
16		prex	$$⊢\left\{A,B\right\}\in \mathrm{V}$$
17		eqeng	$$⊢\left\{A,B\right\}\in \mathrm{V}\to \left(\left\{A,B\right\}=\left\{A,A\right\}\to \left\{A,B\right\}\approx \left\{A,A\right\}\right)$$
18	16 17	ax-mp	$$⊢\left\{A,B\right\}=\left\{A,A\right\}\to \left\{A,B\right\}\approx \left\{A,A\right\}$$
19	15 18	syl11	$$⊢\left\{A,A\right\}\approx 1_{𝑜}\to \left(\left\{A,B\right\}=\left\{A,A\right\}\to \left(\left(A\in C\wedge B\in D\right)\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)\right)$$
20	19	a1dd	$$⊢\left\{A,A\right\}\approx 1_{𝑜}\to \left(\left\{A,B\right\}=\left\{A,A\right\}\to \left(B\in D\to \left(\left(A\in C\wedge B\in D\right)\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)\right)\right)$$
21	3 20	syl	$$⊢A\in C\to \left(\left\{A,B\right\}=\left\{A,A\right\}\to \left(B\in D\to \left(\left(A\in C\wedge B\in D\right)\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)\right)\right)$$
22	21	com23	$$⊢A\in C\to \left(B\in D\to \left(\left\{A,B\right\}=\left\{A,A\right\}\to \left(\left(A\in C\wedge B\in D\right)\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)\right)\right)$$
23	22	imp	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A,B\right\}=\left\{A,A\right\}\to \left(\left(A\in C\wedge B\in D\right)\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)\right)$$
24	23	pm2.43a	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A,B\right\}=\left\{A,A\right\}\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)$$
25	2 24	syl5	$$⊢\left(A\in C\wedge B\in D\right)\to \left(A=B\to \neg \left\{A,B\right\}\approx 2_{𝑜}\right)$$
26	25	necon2ad	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A,B\right\}\approx 2_{𝑜}\to A\ne B\right)$$
27		pr2nelem	$$⊢\left(A\in C\wedge B\in D\wedge A\ne B\right)\to \left\{A,B\right\}\approx 2_{𝑜}$$
28	27	3expia	$$⊢\left(A\in C\wedge B\in D\right)\to \left(A\ne B\to \left\{A,B\right\}\approx 2_{𝑜}\right)$$
29	26 28	impbid	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A,B\right\}\approx 2_{𝑜}\leftrightarrow A\ne B\right)$$