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 } i^i { D , E , F } ) = (/) )

Proof

Step Hyp Ref Expression
1 df-tp 
 |-  { D , E , F } = ( { D , E } u. { F } )
2 1 ineq2i 
 |-  ( { A , B , C } i^i { D , E , F } ) = ( { A , B , C } i^i ( { D , E } u. { F } ) )
3 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
4 3 ineq1i 
 |-  ( { A , B , C } i^i { D , E } ) = ( ( { A , B } u. { C } ) i^i { 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 } i^i { D , E } ) = (/) )
8 5 6 7 syl2an 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) ) -> ( { A , B } i^i { 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 } i^i { D , E } ) = (/) )
10 incom 
 |-  ( { C } i^i { D , E } ) = ( { D , E } i^i { 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 } i^i { C } ) = (/) )
18 13 16 17 syl2an 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) ) -> ( { D , E } i^i { C } ) = (/) )
19 18 3adant3 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) /\ ( A =/= F /\ B =/= F /\ C =/= F ) ) -> ( { D , E } i^i { C } ) = (/) )
20 10 19 eqtrid 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) /\ ( A =/= F /\ B =/= F /\ C =/= F ) ) -> ( { C } i^i { 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 } i^i { D , E } ) = (/) /\ ( { C } i^i { D , E } ) = (/) ) )
22 undisj1 
 |-  ( ( ( { A , B } i^i { D , E } ) = (/) /\ ( { C } i^i { D , E } ) = (/) ) <-> ( ( { A , B } u. { C } ) i^i { 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 } u. { C } ) i^i { D , E } ) = (/) )
24 4 23 eqtrid 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) /\ ( A =/= F /\ B =/= F /\ C =/= F ) ) -> ( { A , B , C } i^i { D , E } ) = (/) )
25 disjtpsn 
 |-  ( ( A =/= F /\ B =/= F /\ C =/= F ) -> ( { A , B , C } i^i { 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 } i^i { 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 } i^i { D , E } ) = (/) /\ ( { A , B , C } i^i { F } ) = (/) ) )
28 undisj2 
 |-  ( ( ( { A , B , C } i^i { D , E } ) = (/) /\ ( { A , B , C } i^i { F } ) = (/) ) <-> ( { A , B , C } i^i ( { D , E } u. { 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 } i^i ( { D , E } u. { F } ) ) = (/) )
30 2 29 eqtrid 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) /\ ( A =/= F /\ B =/= F /\ C =/= F ) ) -> ( { A , B , C } i^i { D , E , F } ) = (/) )