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

Theorem uneqdifeq 3868
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 3590 . . . . 5  |-  ( B  u.  A )  =  ( A  u.  B
)
2 eqtr 2481 . . . . . . 7  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  ( B  u.  A )  =  C )
32eqcomd 2468 . . . . . 6  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  C  =  ( B  u.  A ) )
4 difeq1 3556 . . . . . . 7  |-  ( C  =  ( B  u.  A )  ->  ( C  \  A )  =  ( ( B  u.  A )  \  A
) )
5 difun2 3859 . . . . . . 7  |-  ( ( B  u.  A ) 
\  A )  =  ( B  \  A
)
6 eqtr 2481 . . . . . . . 8  |-  ( ( ( C  \  A
)  =  ( ( B  u.  A ) 
\  A )  /\  ( ( B  u.  A )  \  A
)  =  ( B 
\  A ) )  ->  ( C  \  A )  =  ( B  \  A ) )
7 incom 3637 . . . . . . . . . . 11  |-  ( A  i^i  B )  =  ( B  i^i  A
)
87eqeq1i 2467 . . . . . . . . . 10  |-  ( ( A  i^i  B )  =  (/)  <->  ( B  i^i  A )  =  (/) )
9 disj3 3821 . . . . . . . . . 10  |-  ( ( B  i^i  A )  =  (/)  <->  B  =  ( B  \  A ) )
108, 9bitri 257 . . . . . . . . 9  |-  ( ( A  i^i  B )  =  (/)  <->  B  =  ( B  \  A ) )
11 eqtr 2481 . . . . . . . . . . 11  |-  ( ( ( C  \  A
)  =  ( B 
\  A )  /\  ( B  \  A )  =  B )  -> 
( C  \  A
)  =  B )
1211expcom 441 . . . . . . . . . 10  |-  ( ( B  \  A )  =  B  ->  (
( C  \  A
)  =  ( B 
\  A )  -> 
( C  \  A
)  =  B ) )
1312eqcoms 2470 . . . . . . . . 9  |-  ( B  =  ( B  \  A )  ->  (
( C  \  A
)  =  ( B 
\  A )  -> 
( C  \  A
)  =  B ) )
1410, 13sylbi 200 . . . . . . . 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 673 . . . . . 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 681 . . . 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 472 . 2  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( A  u.  B
)  =  C  -> 
( C  \  A
)  =  B ) )
21 difss 3572 . . . . . . . 8  |-  ( C 
\  A )  C_  C
22 sseq1 3465 . . . . . . . . 9  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  <->  B  C_  C
) )
23 unss 3620 . . . . . . . . . . 11  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
2423biimpi 199 . . . . . . . . . 10  |-  ( ( A  C_  C  /\  B  C_  C )  -> 
( A  u.  B
)  C_  C )
2524expcom 441 . . . . . . . . 9  |-  ( B 
C_  C  ->  ( A  C_  C  ->  ( A  u.  B )  C_  C ) )
2622, 25syl6bi 236 . . . . . . . 8  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  ->  ( A  C_  C  ->  ( A  u.  B ) 
C_  C ) ) )
2721, 26mpi 20 . . . . . . 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 471 . . . . 5  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  C_  C )
)
3029imp 435 . . . 4  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  -> 
( A  u.  B
)  C_  C )
31 eqimss 3496 . . . . . . 7  |-  ( ( C  \  A )  =  B  ->  ( C  \  A )  C_  B )
3231adantl 472 . . . . . 6  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  -> 
( C  \  A
)  C_  B )
33 ssundif 3863 . . . . . 6  |-  ( C 
C_  ( A  u.  B )  <->  ( C  \  A )  C_  B
)
3432, 33sylibr 217 . . . . 5  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  ->  C  C_  ( A  u.  B ) )
3534adantlr 726 . . . 4  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  ->  C  C_  ( A  u.  B ) )
3630, 35eqssd 3461 . . 3  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  -> 
( A  u.  B
)  =  C )
3736ex 440 . 2  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  =  C ) )
3820, 37impbid 195 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 189    /\ wa 375    = wceq 1455    \ cdif 3413    u. cun 3414    i^i cin 3415    C_ wss 3416   (/)c0 3743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744
This theorem is referenced by:  fzdifsuc  11884  hashbclem  12648  lecldbas  20284  conndisj  20480  ptuncnv  20871  ptunhmeo  20872  cldsubg  21174  icopnfcld  21837  iocmnfcld  21838  voliunlem1  22552  icombl  22566  ioombl  22567  uniioombllem4  22593  ismbf3d  22659  lhop  23017  subfacp1lem3  29954  subfacp1lem5  29956  pconcon  30003  cvmscld  30045
  Copyright terms: Public domain W3C validator