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→ABC∩DEF=∅

Proof

Step Hyp Ref Expression
1 df-tp ⊢DEF=DE∪F
2 1 ineq2i ⊢ABC∩DEF=ABC∩DE∪F
3 df-tp ⊢ABC=AB∪C
4 3 ineq1i ⊢ABC∩DE=AB∪C∩DE
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→AB∩DE=∅
8 5 6 7 syl2an ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E→AB∩DE=∅
9 8 3adant3 ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→AB∩DE=∅
10 incom ⊢C∩DE=DE∩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→DE∩C=∅
18 13 16 17 syl2an ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E→DE∩C=∅
19 18 3adant3 ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→DE∩C=∅
20 10 19 eqtrid ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→C∩DE=∅
21 9 20 jca ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→AB∩DE=∅∧C∩DE=∅
22 undisj1 ⊢AB∩DE=∅∧C∩DE=∅↔AB∪C∩DE=∅
23 21 22 sylib ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→AB∪C∩DE=∅
24 4 23 eqtrid ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→ABC∩DE=∅
25 disjtpsn ⊢A≠F∧B≠F∧C≠F→ABC∩F=∅
26 25 3ad2ant3 ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→ABC∩F=∅
27 24 26 jca ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→ABC∩DE=∅∧ABC∩F=∅
28 undisj2 ⊢ABC∩DE=∅∧ABC∩F=∅↔ABC∩DE∪F=∅
29 27 28 sylib ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→ABC∩DE∪F=∅
30 2 29 eqtrid ⊢A≠D∧B≠D∧C≠D∧A≠E∧B≠E∧C≠E∧A≠F∧B≠F∧C≠F→ABC∩DEF=∅