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 ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ∅ )

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
2 1 ineq2i ⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ( { 𝐴 , 𝐵 } ∩ ( { 𝐶 } ∪ { 𝐷 } ) )
3 indi ⊢ ( { 𝐴 , 𝐵 } ∩ ( { 𝐶 } ∪ { 𝐷 } ) ) = ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) ∪ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) )
4 2 3 eqtri ⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) ∪ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) )
5 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
6 5 ineq1i ⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐶 } )
7 indir ⊢ ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐶 } ) = ( ( { 𝐴 } ∩ { 𝐶 } ) ∪ ( { 𝐵 } ∩ { 𝐶 } ) )
8 6 7 eqtri ⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ( ( { 𝐴 } ∩ { 𝐶 } ) ∪ ( { 𝐵 } ∩ { 𝐶 } ) )
9 disjsn2 ⊢ ( 𝐴 ≠ 𝐶 → ( { 𝐴 } ∩ { 𝐶 } ) = ∅ )
10 disjsn2 ⊢ ( 𝐵 ≠ 𝐶 → ( { 𝐵 } ∩ { 𝐶 } ) = ∅ )
11 9 10 anim12i ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐶 } ) = ∅ ) )
12 un00 ⊢ ( ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐶 } ) = ∅ ) ↔ ( ( { 𝐴 } ∩ { 𝐶 } ) ∪ ( { 𝐵 } ∩ { 𝐶 } ) ) = ∅ )
13 11 12 sylib ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( { 𝐴 } ∩ { 𝐶 } ) ∪ ( { 𝐵 } ∩ { 𝐶 } ) ) = ∅ )
14 8 13 syl5eq ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )
15 14 adantr ⊢ ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )
16 5 ineq1i ⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐷 } )
17 indir ⊢ ( ( { 𝐴 } ∪ { 𝐵 } ) ∩ { 𝐷 } ) = ( ( { 𝐴 } ∩ { 𝐷 } ) ∪ ( { 𝐵 } ∩ { 𝐷 } ) )
18 16 17 eqtri ⊢ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ( ( { 𝐴 } ∩ { 𝐷 } ) ∪ ( { 𝐵 } ∩ { 𝐷 } ) )
19 disjsn2 ⊢ ( 𝐴 ≠ 𝐷 → ( { 𝐴 } ∩ { 𝐷 } ) = ∅ )
20 disjsn2 ⊢ ( 𝐵 ≠ 𝐷 → ( { 𝐵 } ∩ { 𝐷 } ) = ∅ )
21 19 20 anim12i ⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) → ( ( { 𝐴 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐷 } ) = ∅ ) )
22 un00 ⊢ ( ( ( { 𝐴 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐷 } ) = ∅ ) ↔ ( ( { 𝐴 } ∩ { 𝐷 } ) ∪ ( { 𝐵 } ∩ { 𝐷 } ) ) = ∅ )
23 21 22 sylib ⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) → ( ( { 𝐴 } ∩ { 𝐷 } ) ∪ ( { 𝐵 } ∩ { 𝐷 } ) ) = ∅ )
24 18 23 syl5eq ⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ )
25 24 adantl ⊢ ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ )
26 15 25 uneq12d ⊢ ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) ) → ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) ∪ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) ) = ( ∅ ∪ ∅ ) )
27 un0 ⊢ ( ∅ ∪ ∅ ) = ∅
28 26 27 eqtrdi ⊢ ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) ) → ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) ∪ ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) ) = ∅ )
29 4 28 syl5eq ⊢ ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 , 𝐷 } ) = ∅ )