Metamath Proof Explorer

Theorem disjtpsn

Description: The disjoint intersection of an unordered triple and a singleton. (Contributed by AV, 14-Nov-2021)

Ref Expression
Assertion disjtpsn 
|- ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { A , B , C } i^i { D } ) = (/) )

Proof

Step Hyp Ref Expression
1 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
2 1 ineq1i 
 |-  ( { A , B , C } i^i { D } ) = ( ( { A , B } u. { C } ) i^i { D } )
3 disjprsn 
 |-  ( ( A =/= D /\ B =/= D ) -> ( { A , B } i^i { D } ) = (/) )
4 3 3adant3 
 |-  ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { A , B } i^i { D } ) = (/) )
5 disjsn2 
 |-  ( C =/= D -> ( { C } i^i { D } ) = (/) )
6 5 3ad2ant3 
 |-  ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { C } i^i { D } ) = (/) )
7 4 6 jca 
 |-  ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( ( { A , B } i^i { D } ) = (/) /\ ( { C } i^i { D } ) = (/) ) )
8 undisj1 
 |-  ( ( ( { A , B } i^i { D } ) = (/) /\ ( { C } i^i { D } ) = (/) ) <-> ( ( { A , B } u. { C } ) i^i { D } ) = (/) )
9 7 8 sylib 
 |-  ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( ( { A , B } u. { C } ) i^i { D } ) = (/) )
10 2 9 syl5eq 
 |-  ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { A , B , C } i^i { D } ) = (/) )