Theorem pr2nelem

Description: Lemma for pr2ne . (Contributed by FL, 17-Aug-2008)

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

Proof

Step	Hyp	Ref	Expression
1		disjsn2	$$⊢A\ne B\to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
2		ensn1g	$$⊢A\in C\to \left\{A\right\}\approx 1_{𝑜}$$
3		ensn1g	$$⊢B\in D\to \left\{B\right\}\approx 1_{𝑜}$$
4		pm54.43	$$⊢\left(\left\{A\right\}\approx 1_{𝑜}\wedge \left\{B\right\}\approx 1_{𝑜}\right)\to \left(\left\{A\right\}\cap \left\{B\right\}=\varnothing \leftrightarrow \left(\left\{A\right\}\cup \left\{B\right\}\right)\approx 2_{𝑜}\right)$$
5		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
6	5	breq1i	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\leftrightarrow \left(\left\{A\right\}\cup \left\{B\right\}\right)\approx 2_{𝑜}$$
7	4 6	bitr4di	$$⊢\left(\left\{A\right\}\approx 1_{𝑜}\wedge \left\{B\right\}\approx 1_{𝑜}\right)\to \left(\left\{A\right\}\cap \left\{B\right\}=\varnothing \leftrightarrow \left\{A,B\right\}\approx 2_{𝑜}\right)$$
8	7	biimpd	$$⊢\left(\left\{A\right\}\approx 1_{𝑜}\wedge \left\{B\right\}\approx 1_{𝑜}\right)\to \left(\left\{A\right\}\cap \left\{B\right\}=\varnothing \to \left\{A,B\right\}\approx 2_{𝑜}\right)$$
9	2 3 8	syl2an	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A\right\}\cap \left\{B\right\}=\varnothing \to \left\{A,B\right\}\approx 2_{𝑜}\right)$$
10	9	ex	$$⊢A\in C\to \left(B\in D\to \left(\left\{A\right\}\cap \left\{B\right\}=\varnothing \to \left\{A,B\right\}\approx 2_{𝑜}\right)\right)$$
11	1 10	syl7	$$⊢A\in C\to \left(B\in D\to \left(A\ne B\to \left\{A,B\right\}\approx 2_{𝑜}\right)\right)$$
12	11	3imp	$$⊢\left(A\in C\wedge B\in D\wedge A\ne B\right)\to \left\{A,B\right\}\approx 2_{𝑜}$$