# Metamath Proof Explorer

## 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)↔\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)↔\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$