This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjpr2

Description: Two completely distinct unordered pairs are disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017) (Proof shortened by JJ, 23-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { C , D } = ( { C } u. { D } )
2 1 ineq2i 
 |-  ( { A , B } i^i { C , D } ) = ( { A , B } i^i ( { C } u. { D } ) )
3 indi 
 |-  ( { A , B } i^i ( { C } u. { D } ) ) = ( ( { A , B } i^i { C } ) u. ( { A , B } i^i { D } ) )
4 2 3 eqtri 
 |-  ( { A , B } i^i { C , D } ) = ( ( { A , B } i^i { C } ) u. ( { A , B } i^i { D } ) )
5 df-pr 
 |-  { A , B } = ( { A } u. { B } )
6 5 ineq1i 
 |-  ( { A , B } i^i { C } ) = ( ( { A } u. { B } ) i^i { C } )
7 indir 
 |-  ( ( { A } u. { B } ) i^i { C } ) = ( ( { A } i^i { C } ) u. ( { B } i^i { C } ) )
8 6 7 eqtri 
 |-  ( { A , B } i^i { C } ) = ( ( { A } i^i { C } ) u. ( { B } i^i { C } ) )
9 disjsn2 
 |-  ( A =/= C -> ( { A } i^i { C } ) = (/) )
10 disjsn2 
 |-  ( B =/= C -> ( { B } i^i { C } ) = (/) )
11 9 10 anim12i 
 |-  ( ( A =/= C /\ B =/= C ) -> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) )
12 un00 
 |-  ( ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) <-> ( ( { A } i^i { C } ) u. ( { B } i^i { C } ) ) = (/) )
13 11 12 sylib 
 |-  ( ( A =/= C /\ B =/= C ) -> ( ( { A } i^i { C } ) u. ( { B } i^i { C } ) ) = (/) )
14 8 13 eqtrid 
 |-  ( ( A =/= C /\ B =/= C ) -> ( { A , B } i^i { C } ) = (/) )
15 14 adantr 
 |-  ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { C } ) = (/) )
16 5 ineq1i 
 |-  ( { A , B } i^i { D } ) = ( ( { A } u. { B } ) i^i { D } )
17 indir 
 |-  ( ( { A } u. { B } ) i^i { D } ) = ( ( { A } i^i { D } ) u. ( { B } i^i { D } ) )
18 16 17 eqtri 
 |-  ( { A , B } i^i { D } ) = ( ( { A } i^i { D } ) u. ( { B } i^i { D } ) )
19 disjsn2 
 |-  ( A =/= D -> ( { A } i^i { D } ) = (/) )
20 disjsn2 
 |-  ( B =/= D -> ( { B } i^i { D } ) = (/) )
21 19 20 anim12i 
 |-  ( ( A =/= D /\ B =/= D ) -> ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) )
22 un00 
 |-  ( ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) <-> ( ( { A } i^i { D } ) u. ( { B } i^i { D } ) ) = (/) )
23 21 22 sylib 
 |-  ( ( A =/= D /\ B =/= D ) -> ( ( { A } i^i { D } ) u. ( { B } i^i { D } ) ) = (/) )
24 18 23 eqtrid 
 |-  ( ( A =/= D /\ B =/= D ) -> ( { A , B } i^i { D } ) = (/) )
25 24 adantl 
 |-  ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { D } ) = (/) )
26 15 25 uneq12d 
 |-  ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( ( { A , B } i^i { C } ) u. ( { A , B } i^i { D } ) ) = ( (/) u. (/) ) )
27 un0 
 |-  ( (/) u. (/) ) = (/)
28 26 27 eqtrdi 
 |-  ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( ( { A , B } i^i { C } ) u. ( { A , B } i^i { D } ) ) = (/) )
29 4 28 eqtrid 
 |-  ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { C , D } ) = (/) )