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

Theorem uneqdifeq 3788
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 3521 . . . . 5  |-  ( B  u.  A )  =  ( A  u.  B
)
2 eqtr 2460 . . . . . . 7  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  ( B  u.  A )  =  C )
32eqcomd 2448 . . . . . 6  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  C  =  ( B  u.  A ) )
4 difeq1 3488 . . . . . . 7  |-  ( C  =  ( B  u.  A )  ->  ( C  \  A )  =  ( ( B  u.  A )  \  A
) )
5 difun2 3779 . . . . . . 7  |-  ( ( B  u.  A ) 
\  A )  =  ( B  \  A
)
6 eqtr 2460 . . . . . . . 8  |-  ( ( ( C  \  A
)  =  ( ( B  u.  A ) 
\  A )  /\  ( ( B  u.  A )  \  A
)  =  ( B 
\  A ) )  ->  ( C  \  A )  =  ( B  \  A ) )
7 incom 3564 . . . . . . . . . . 11  |-  ( A  i^i  B )  =  ( B  i^i  A
)
87eqeq1i 2450 . . . . . . . . . 10  |-  ( ( A  i^i  B )  =  (/)  <->  ( B  i^i  A )  =  (/) )
9 disj3 3744 . . . . . . . . . 10  |-  ( ( B  i^i  A )  =  (/)  <->  B  =  ( B  \  A ) )
108, 9bitri 249 . . . . . . . . 9  |-  ( ( A  i^i  B )  =  (/)  <->  B  =  ( B  \  A ) )
11 eqtr 2460 . . . . . . . . . . 11  |-  ( ( ( C  \  A
)  =  ( B 
\  A )  /\  ( B  \  A )  =  B )  -> 
( C  \  A
)  =  B )
1211expcom 435 . . . . . . . . . 10  |-  ( ( B  \  A )  =  B  ->  (
( C  \  A
)  =  ( B 
\  A )  -> 
( C  \  A
)  =  B ) )
1312eqcoms 2446 . . . . . . . . 9  |-  ( B  =  ( B  \  A )  ->  (
( C  \  A
)  =  ( B 
\  A )  -> 
( C  \  A
)  =  B ) )
1410, 13sylbi 195 . . . . . . . 8  |-  ( ( A  i^i  B )  =  (/)  ->  ( ( C  \  A )  =  ( B  \  A )  ->  ( C  \  A )  =  B ) )
156, 14syl5com 30 . . . . . . 7  |-  ( ( ( C  \  A
)  =  ( ( B  u.  A ) 
\  A )  /\  ( ( B  u.  A )  \  A
)  =  ( B 
\  A ) )  ->  ( ( A  i^i  B )  =  (/)  ->  ( C  \  A )  =  B ) )
164, 5, 15sylancl 662 . . . . . 6  |-  ( C  =  ( B  u.  A )  ->  (
( A  i^i  B
)  =  (/)  ->  ( C  \  A )  =  B ) )
173, 16syl 16 . . . . 5  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  ( ( A  i^i  B )  =  (/)  ->  ( C  \  A )  =  B ) )
181, 17mpan 670 . . . 4  |-  ( ( A  u.  B )  =  C  ->  (
( A  i^i  B
)  =  (/)  ->  ( C  \  A )  =  B ) )
1918com12 31 . . 3  |-  ( ( A  i^i  B )  =  (/)  ->  ( ( A  u.  B )  =  C  ->  ( C  \  A )  =  B ) )
2019adantl 466 . 2  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( A  u.  B
)  =  C  -> 
( C  \  A
)  =  B ) )
21 difss 3504 . . . . . . . 8  |-  ( C 
\  A )  C_  C
22 sseq1 3398 . . . . . . . . 9  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  <->  B  C_  C
) )
23 unss 3551 . . . . . . . . . . 11  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
2423biimpi 194 . . . . . . . . . 10  |-  ( ( A  C_  C  /\  B  C_  C )  -> 
( A  u.  B
)  C_  C )
2524expcom 435 . . . . . . . . 9  |-  ( B 
C_  C  ->  ( A  C_  C  ->  ( A  u.  B )  C_  C ) )
2622, 25syl6bi 228 . . . . . . . 8  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  ->  ( A  C_  C  ->  ( A  u.  B ) 
C_  C ) ) )
2721, 26mpi 17 . . . . . . 7  |-  ( ( C  \  A )  =  B  ->  ( A  C_  C  ->  ( A  u.  B )  C_  C ) )
2827com12 31 . . . . . 6  |-  ( A 
C_  C  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  C_  C )
)
2928adantr 465 . . . . 5  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  C_  C )
)
3029imp 429 . . . 4  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  -> 
( A  u.  B
)  C_  C )
31 eqimss 3429 . . . . . . 7  |-  ( ( C  \  A )  =  B  ->  ( C  \  A )  C_  B )
3231adantl 466 . . . . . 6  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  -> 
( C  \  A
)  C_  B )
33 ssundif 3783 . . . . . 6  |-  ( C 
C_  ( A  u.  B )  <->  ( C  \  A )  C_  B
)
3432, 33sylibr 212 . . . . 5  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  ->  C  C_  ( A  u.  B ) )
3534adantlr 714 . . . 4  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  ->  C  C_  ( A  u.  B ) )
3630, 35eqssd 3394 . . 3  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  -> 
( A  u.  B
)  =  C )
3736ex 434 . 2  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  =  C ) )
3820, 37impbid 191 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 184    /\ wa 369    = wceq 1369    \ cdif 3346    u. cun 3347    i^i cin 3348    C_ wss 3349   (/)c0 3658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659
This theorem is referenced by:  fzdifsuc  11537  hashbclem  12226  lecldbas  18845  conndisj  19042  ptuncnv  19402  ptunhmeo  19403  cldsubg  19703  icopnfcld  20369  iocmnfcld  20370  voliunlem1  21053  icombl  21067  ioombl  21068  uniioombllem4  21088  ismbf3d  21154  lhop  21510  subfacp1lem3  27092  subfacp1lem5  27094  pconcon  27142  cvmscld  27184
  Copyright terms: Public domain W3C validator