Metamath Proof Explorer

Theorem disjtppr

Description: The disjoint intersection of an unordered triple and an unordered pair. (Contributed by Thierry Arnoux, 9-Nov-2026)

Ref Expression
Assertion disjtppr ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E → A B C ∩ D E = ∅

Proof

Step Hyp Ref Expression
1 df-pr ⊢ D E = D ∪ E
2 1 ineq2i ⊢ A B C ∩ D E = A B C ∩ D ∪ E
3 disjtpsn ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → A B C ∩ D = ∅
4 disjtpsn ⊢ A ≠ E ∧ B ≠ E ∧ C ≠ E → A B C ∩ E = ∅
5 3 4 anim12i ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E → A B C ∩ D = ∅ ∧ A B C ∩ E = ∅
6 undisj2 ⊢ A B C ∩ D = ∅ ∧ A B C ∩ E = ∅ ↔ A B C ∩ D ∪ E = ∅
7 5 6 sylib ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E → A B C ∩ D ∪ E = ∅
8 2 7 eqtrid ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E → A B C ∩ D E = ∅