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

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { D , E } = ( { D } u. { E } )
2 1 ineq2i 
 |-  ( { A , B , C } i^i { D , E } ) = ( { A , B , C } i^i ( { D } u. { E } ) )
3 disjtpsn 
 |-  ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { A , B , C } i^i { D } ) = (/) )
4 disjtpsn 
 |-  ( ( A =/= E /\ B =/= E /\ C =/= E ) -> ( { A , B , C } i^i { E } ) = (/) )
5 3 4 anim12i 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) ) -> ( ( { A , B , C } i^i { D } ) = (/) /\ ( { A , B , C } i^i { E } ) = (/) ) )
6 undisj2 
 |-  ( ( ( { A , B , C } i^i { D } ) = (/) /\ ( { A , B , C } i^i { E } ) = (/) ) <-> ( { A , B , C } i^i ( { D } u. { E } ) ) = (/) )
7 5 6 sylib 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) ) -> ( { A , B , C } i^i ( { D } u. { E } ) ) = (/) )
8 2 7 eqtrid 
 |-  ( ( ( A =/= D /\ B =/= D /\ C =/= D ) /\ ( A =/= E /\ B =/= E /\ C =/= E ) ) -> ( { A , B , C } i^i { D , E } ) = (/) )