Theorem disjpr2

Description: Two completely distinct unordered pairs are disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017) (Proof shortened by JJ, 23-Jul-2021)

	Ref	Expression
Assertion	disjpr2	$$⊢\left(\left(A\ne C\wedge B\ne C\right)\wedge \left(A\ne D\wedge B\ne D\right)\right)\to \left\{A,B\right\}\cap \left\{C,D\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{C,D\right\}=\left\{C\right\}\cup \left\{D\right\}$$
2	1	ineq2i	$$⊢\left\{A,B\right\}\cap \left\{C,D\right\}=\left\{A,B\right\}\cap \left(\left\{C\right\}\cup \left\{D\right\}\right)$$
3		indi	$$⊢\left\{A,B\right\}\cap \left(\left\{C\right\}\cup \left\{D\right\}\right)=\left(\left\{A,B\right\}\cap \left\{C\right\}\right)\cup \left(\left\{A,B\right\}\cap \left\{D\right\}\right)$$
4	2 3	eqtri	$$⊢\left\{A,B\right\}\cap \left\{C,D\right\}=\left(\left\{A,B\right\}\cap \left\{C\right\}\right)\cup \left(\left\{A,B\right\}\cap \left\{D\right\}\right)$$
5		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
6	5	ineq1i	$$⊢\left\{A,B\right\}\cap \left\{C\right\}=\left(\left\{A\right\}\cup \left\{B\right\}\right)\cap \left\{C\right\}$$
7		indir	$$⊢\left(\left\{A\right\}\cup \left\{B\right\}\right)\cap \left\{C\right\}=\left(\left\{A\right\}\cap \left\{C\right\}\right)\cup \left(\left\{B\right\}\cap \left\{C\right\}\right)$$
8	6 7	eqtri	$$⊢\left\{A,B\right\}\cap \left\{C\right\}=\left(\left\{A\right\}\cap \left\{C\right\}\right)\cup \left(\left\{B\right\}\cap \left\{C\right\}\right)$$
9		disjsn2	$$⊢A\ne C\to \left\{A\right\}\cap \left\{C\right\}=\varnothing$$
10		disjsn2	$$⊢B\ne C\to \left\{B\right\}\cap \left\{C\right\}=\varnothing$$
11	9 10	anim12i	$$⊢\left(A\ne C\wedge B\ne C\right)\to \left(\left\{A\right\}\cap \left\{C\right\}=\varnothing \wedge \left\{B\right\}\cap \left\{C\right\}=\varnothing \right)$$
12		un00	$$⊢\left(\left\{A\right\}\cap \left\{C\right\}=\varnothing \wedge \left\{B\right\}\cap \left\{C\right\}=\varnothing \right)\leftrightarrow \left(\left\{A\right\}\cap \left\{C\right\}\right)\cup \left(\left\{B\right\}\cap \left\{C\right\}\right)=\varnothing$$
13	11 12	sylib	$$⊢\left(A\ne C\wedge B\ne C\right)\to \left(\left\{A\right\}\cap \left\{C\right\}\right)\cup \left(\left\{B\right\}\cap \left\{C\right\}\right)=\varnothing$$
14	8 13	syl5eq	$$⊢\left(A\ne C\wedge B\ne C\right)\to \left\{A,B\right\}\cap \left\{C\right\}=\varnothing$$
15	14	adantr	$$⊢\left(\left(A\ne C\wedge B\ne C\right)\wedge \left(A\ne D\wedge B\ne D\right)\right)\to \left\{A,B\right\}\cap \left\{C\right\}=\varnothing$$
16	5	ineq1i	$$⊢\left\{A,B\right\}\cap \left\{D\right\}=\left(\left\{A\right\}\cup \left\{B\right\}\right)\cap \left\{D\right\}$$
17		indir	$$⊢\left(\left\{A\right\}\cup \left\{B\right\}\right)\cap \left\{D\right\}=\left(\left\{A\right\}\cap \left\{D\right\}\right)\cup \left(\left\{B\right\}\cap \left\{D\right\}\right)$$
18	16 17	eqtri	$$⊢\left\{A,B\right\}\cap \left\{D\right\}=\left(\left\{A\right\}\cap \left\{D\right\}\right)\cup \left(\left\{B\right\}\cap \left\{D\right\}\right)$$
19		disjsn2	$$⊢A\ne D\to \left\{A\right\}\cap \left\{D\right\}=\varnothing$$
20		disjsn2	$$⊢B\ne D\to \left\{B\right\}\cap \left\{D\right\}=\varnothing$$
21	19 20	anim12i	$$⊢\left(A\ne D\wedge B\ne D\right)\to \left(\left\{A\right\}\cap \left\{D\right\}=\varnothing \wedge \left\{B\right\}\cap \left\{D\right\}=\varnothing \right)$$
22		un00	$$⊢\left(\left\{A\right\}\cap \left\{D\right\}=\varnothing \wedge \left\{B\right\}\cap \left\{D\right\}=\varnothing \right)\leftrightarrow \left(\left\{A\right\}\cap \left\{D\right\}\right)\cup \left(\left\{B\right\}\cap \left\{D\right\}\right)=\varnothing$$
23	21 22	sylib	$$⊢\left(A\ne D\wedge B\ne D\right)\to \left(\left\{A\right\}\cap \left\{D\right\}\right)\cup \left(\left\{B\right\}\cap \left\{D\right\}\right)=\varnothing$$
24	18 23	syl5eq	$$⊢\left(A\ne D\wedge B\ne D\right)\to \left\{A,B\right\}\cap \left\{D\right\}=\varnothing$$
25	24	adantl	$$⊢\left(\left(A\ne C\wedge B\ne C\right)\wedge \left(A\ne D\wedge B\ne D\right)\right)\to \left\{A,B\right\}\cap \left\{D\right\}=\varnothing$$
26	15 25	uneq12d	$$⊢\left(\left(A\ne C\wedge B\ne C\right)\wedge \left(A\ne D\wedge B\ne D\right)\right)\to \left(\left\{A,B\right\}\cap \left\{C\right\}\right)\cup \left(\left\{A,B\right\}\cap \left\{D\right\}\right)=\varnothing \cup \varnothing$$
27		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
28	26 27	eqtrdi	$$⊢\left(\left(A\ne C\wedge B\ne C\right)\wedge \left(A\ne D\wedge B\ne D\right)\right)\to \left(\left\{A,B\right\}\cap \left\{C\right\}\right)\cup \left(\left\{A,B\right\}\cap \left\{D\right\}\right)=\varnothing$$
29	4 28	syl5eq	$$⊢\left(\left(A\ne C\wedge B\ne C\right)\wedge \left(A\ne D\wedge B\ne D\right)\right)\to \left\{A,B\right\}\cap \left\{C,D\right\}=\varnothing$$