Metamath Proof Explorer

Theorem disjtp2

Description: Two completely distinct unordered triples are disjoint. (Contributed by AV, 14-Nov-2021)

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

Proof

Step Hyp Ref Expression
1 df-tp ⊢ D E F = D E ∪ F
2 1 ineq2i ⊢ A B C ∩ D E F = A B C ∩ D E ∪ F
3 df-tp ⊢ A B C = A B ∪ C
4 3 ineq1i ⊢ A B C ∩ D E = A B ∪ C ∩ D E
5 3simpa ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → A ≠ D ∧ B ≠ D
6 3simpa ⊢ A ≠ E ∧ B ≠ E ∧ C ≠ E → A ≠ E ∧ B ≠ E
7 disjpr2 ⊢ A ≠ D ∧ B ≠ D ∧ A ≠ E ∧ B ≠ E → A B ∩ D E = ∅
8 5 6 7 syl2an ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E → A B ∩ D E = ∅
9 8 3adant3 ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B ∩ D E = ∅
10 incom ⊢ C ∩ D E = D E ∩ C
11 necom ⊢ C ≠ D ↔ D ≠ C
12 11 biimpi ⊢ C ≠ D → D ≠ C
13 12 3ad2ant3 ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → D ≠ C
14 necom ⊢ C ≠ E ↔ E ≠ C
15 14 biimpi ⊢ C ≠ E → E ≠ C
16 15 3ad2ant3 ⊢ A ≠ E ∧ B ≠ E ∧ C ≠ E → E ≠ C
17 disjprsn ⊢ D ≠ C ∧ E ≠ C → D E ∩ C = ∅
18 13 16 17 syl2an ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E → D E ∩ C = ∅
19 18 3adant3 ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → D E ∩ C = ∅
20 10 19 syl5eq ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → C ∩ D E = ∅
21 9 20 jca ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B ∩ D E = ∅ ∧ C ∩ D E = ∅
22 undisj1 ⊢ A B ∩ D E = ∅ ∧ C ∩ D E = ∅ ↔ A B ∪ C ∩ D E = ∅
23 21 22 sylib ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B ∪ C ∩ D E = ∅
24 4 23 syl5eq ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B C ∩ D E = ∅
25 disjtpsn ⊢ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B C ∩ F = ∅
26 25 3ad2ant3 ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B C ∩ F = ∅
27 24 26 jca ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B C ∩ D E = ∅ ∧ A B C ∩ F = ∅
28 undisj2 ⊢ A B C ∩ D E = ∅ ∧ A B C ∩ F = ∅ ↔ A B C ∩ D E ∪ F = ∅
29 27 28 sylib ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B C ∩ D E ∪ F = ∅
30 2 29 syl5eq ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D ∧ A ≠ E ∧ B ≠ E ∧ C ≠ E ∧ A ≠ F ∧ B ≠ F ∧ C ≠ F → A B C ∩ D E F = ∅