MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneqdifeq Structured version   Unicode version

Theorem uneqdifeq 3884
Description: Two ways to say that  A and  B partition  C (when 
A and  B don't overlap and  A is a part of  C). (Contributed by FL, 17-Nov-2008.)
Assertion
Ref Expression
uneqdifeq  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( A  u.  B
)  =  C  <->  ( C  \  A )  =  B ) )

Proof of Theorem uneqdifeq
StepHypRef Expression
1 uncom 3610 . . . . 5  |-  ( B  u.  A )  =  ( A  u.  B
)
2 eqtr 2448 . . . . . . 7  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  ( B  u.  A )  =  C )
32eqcomd 2430 . . . . . 6  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  C  =  ( B  u.  A ) )
4 difeq1 3576 . . . . . . 7  |-  ( C  =  ( B  u.  A )  ->  ( C  \  A )  =  ( ( B  u.  A )  \  A
) )
5 difun2 3875 . . . . . . 7  |-  ( ( B  u.  A ) 
\  A )  =  ( B  \  A
)
6 eqtr 2448 . . . . . . . 8  |-  ( ( ( C  \  A
)  =  ( ( B  u.  A ) 
\  A )  /\  ( ( B  u.  A )  \  A
)  =  ( B 
\  A ) )  ->  ( C  \  A )  =  ( B  \  A ) )
7 incom 3655 . . . . . . . . . . 11  |-  ( A  i^i  B )  =  ( B  i^i  A
)
87eqeq1i 2429 . . . . . . . . . 10  |-  ( ( A  i^i  B )  =  (/)  <->  ( B  i^i  A )  =  (/) )
9 disj3 3837 . . . . . . . . . 10  |-  ( ( B  i^i  A )  =  (/)  <->  B  =  ( B  \  A ) )
108, 9bitri 252 . . . . . . . . 9  |-  ( ( A  i^i  B )  =  (/)  <->  B  =  ( B  \  A ) )
11 eqtr 2448 . . . . . . . . . . 11  |-  ( ( ( C  \  A
)  =  ( B 
\  A )  /\  ( B  \  A )  =  B )  -> 
( C  \  A
)  =  B )
1211expcom 436 . . . . . . . . . 10  |-  ( ( B  \  A )  =  B  ->  (
( C  \  A
)  =  ( B 
\  A )  -> 
( C  \  A
)  =  B ) )
1312eqcoms 2434 . . . . . . . . 9  |-  ( B  =  ( B  \  A )  ->  (
( C  \  A
)  =  ( B 
\  A )  -> 
( C  \  A
)  =  B ) )
1410, 13sylbi 198 . . . . . . . 8  |-  ( ( A  i^i  B )  =  (/)  ->  ( ( C  \  A )  =  ( B  \  A )  ->  ( C  \  A )  =  B ) )
156, 14syl5com 31 . . . . . . 7  |-  ( ( ( C  \  A
)  =  ( ( B  u.  A ) 
\  A )  /\  ( ( B  u.  A )  \  A
)  =  ( B 
\  A ) )  ->  ( ( A  i^i  B )  =  (/)  ->  ( C  \  A )  =  B ) )
164, 5, 15sylancl 666 . . . . . 6  |-  ( C  =  ( B  u.  A )  ->  (
( A  i^i  B
)  =  (/)  ->  ( C  \  A )  =  B ) )
173, 16syl 17 . . . . 5  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  ( ( A  i^i  B )  =  (/)  ->  ( C  \  A )  =  B ) )
181, 17mpan 674 . . . 4  |-  ( ( A  u.  B )  =  C  ->  (
( A  i^i  B
)  =  (/)  ->  ( C  \  A )  =  B ) )
1918com12 32 . . 3  |-  ( ( A  i^i  B )  =  (/)  ->  ( ( A  u.  B )  =  C  ->  ( C  \  A )  =  B ) )
2019adantl 467 . 2  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( A  u.  B
)  =  C  -> 
( C  \  A
)  =  B ) )
21 difss 3592 . . . . . . . 8  |-  ( C 
\  A )  C_  C
22 sseq1 3485 . . . . . . . . 9  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  <->  B  C_  C
) )
23 unss 3640 . . . . . . . . . . 11  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
2423biimpi 197 . . . . . . . . . 10  |-  ( ( A  C_  C  /\  B  C_  C )  -> 
( A  u.  B
)  C_  C )
2524expcom 436 . . . . . . . . 9  |-  ( B 
C_  C  ->  ( A  C_  C  ->  ( A  u.  B )  C_  C ) )
2622, 25syl6bi 231 . . . . . . . 8  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  ->  ( A  C_  C  ->  ( A  u.  B ) 
C_  C ) ) )
2721, 26mpi 21 . . . . . . 7  |-  ( ( C  \  A )  =  B  ->  ( A  C_  C  ->  ( A  u.  B )  C_  C ) )
2827com12 32 . . . . . 6  |-  ( A 
C_  C  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  C_  C )
)
2928adantr 466 . . . . 5  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  C_  C )
)
3029imp 430 . . . 4  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  -> 
( A  u.  B
)  C_  C )
31 eqimss 3516 . . . . . . 7  |-  ( ( C  \  A )  =  B  ->  ( C  \  A )  C_  B )
3231adantl 467 . . . . . 6  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  -> 
( C  \  A
)  C_  B )
33 ssundif 3879 . . . . . 6  |-  ( C 
C_  ( A  u.  B )  <->  ( C  \  A )  C_  B
)
3432, 33sylibr 215 . . . . 5  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  ->  C  C_  ( A  u.  B ) )
3534adantlr 719 . . . 4  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  ->  C  C_  ( A  u.  B ) )
3630, 35eqssd 3481 . . 3  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  -> 
( A  u.  B
)  =  C )
3736ex 435 . 2  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  =  C ) )
3820, 37impbid 193 1  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( A  u.  B
)  =  C  <->  ( C  \  A )  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    \ cdif 3433    u. cun 3434    i^i cin 3435    C_ wss 3436   (/)c0 3761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762
This theorem is referenced by:  fzdifsuc  11855  hashbclem  12612  lecldbas  20221  conndisj  20417  ptuncnv  20808  ptunhmeo  20809  cldsubg  21111  icopnfcld  21774  iocmnfcld  21775  voliunlem1  22489  icombl  22503  ioombl  22504  uniioombllem4  22530  ismbf3d  22596  lhop  22954  subfacp1lem3  29900  subfacp1lem5  29902  pconcon  29949  cvmscld  29991
  Copyright terms: Public domain W3C validator