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

Theorem uneqdifeq 3542
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 3319 . . . . 5  |-  ( B  u.  A )  =  ( A  u.  B
)
2 eqtr 2300 . . . . . . 7  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  ( B  u.  A )  =  C )
32eqcomd 2288 . . . . . 6  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  C  =  ( B  u.  A ) )
4 difeq1 3287 . . . . . . 7  |-  ( C  =  ( B  u.  A )  ->  ( C  \  A )  =  ( ( B  u.  A )  \  A
) )
5 difun2 3533 . . . . . . 7  |-  ( ( B  u.  A ) 
\  A )  =  ( B  \  A
)
6 eqtr 2300 . . . . . . . 8  |-  ( ( ( C  \  A
)  =  ( ( B  u.  A ) 
\  A )  /\  ( ( B  u.  A )  \  A
)  =  ( B 
\  A ) )  ->  ( C  \  A )  =  ( B  \  A ) )
7 incom 3361 . . . . . . . . . . 11  |-  ( A  i^i  B )  =  ( B  i^i  A
)
87eqeq1i 2290 . . . . . . . . . 10  |-  ( ( A  i^i  B )  =  (/)  <->  ( B  i^i  A )  =  (/) )
9 disj3 3499 . . . . . . . . . 10  |-  ( ( B  i^i  A )  =  (/)  <->  B  =  ( B  \  A ) )
108, 9bitri 240 . . . . . . . . 9  |-  ( ( A  i^i  B )  =  (/)  <->  B  =  ( B  \  A ) )
11 eqtr 2300 . . . . . . . . . . 11  |-  ( ( ( C  \  A
)  =  ( B 
\  A )  /\  ( B  \  A )  =  B )  -> 
( C  \  A
)  =  B )
1211expcom 424 . . . . . . . . . 10  |-  ( ( B  \  A )  =  B  ->  (
( C  \  A
)  =  ( B 
\  A )  -> 
( C  \  A
)  =  B ) )
1312eqcoms 2286 . . . . . . . . 9  |-  ( B  =  ( B  \  A )  ->  (
( C  \  A
)  =  ( B 
\  A )  -> 
( C  \  A
)  =  B ) )
1410, 13sylbi 187 . . . . . . . 8  |-  ( ( A  i^i  B )  =  (/)  ->  ( ( C  \  A )  =  ( B  \  A )  ->  ( C  \  A )  =  B ) )
156, 14syl5com 26 . . . . . . 7  |-  ( ( ( C  \  A
)  =  ( ( B  u.  A ) 
\  A )  /\  ( ( B  u.  A )  \  A
)  =  ( B 
\  A ) )  ->  ( ( A  i^i  B )  =  (/)  ->  ( C  \  A )  =  B ) )
164, 5, 15sylancl 643 . . . . . 6  |-  ( C  =  ( B  u.  A )  ->  (
( A  i^i  B
)  =  (/)  ->  ( C  \  A )  =  B ) )
173, 16syl 15 . . . . 5  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  ( ( A  i^i  B )  =  (/)  ->  ( C  \  A )  =  B ) )
181, 17mpan 651 . . . 4  |-  ( ( A  u.  B )  =  C  ->  (
( A  i^i  B
)  =  (/)  ->  ( C  \  A )  =  B ) )
1918com12 27 . . 3  |-  ( ( A  i^i  B )  =  (/)  ->  ( ( A  u.  B )  =  C  ->  ( C  \  A )  =  B ) )
2019adantl 452 . 2  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( A  u.  B
)  =  C  -> 
( C  \  A
)  =  B ) )
21 difss 3303 . . . . . . . 8  |-  ( C 
\  A )  C_  C
22 sseq1 3199 . . . . . . . . 9  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  <->  B  C_  C
) )
23 unss 3349 . . . . . . . . . . 11  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
2423biimpi 186 . . . . . . . . . 10  |-  ( ( A  C_  C  /\  B  C_  C )  -> 
( A  u.  B
)  C_  C )
2524expcom 424 . . . . . . . . 9  |-  ( B 
C_  C  ->  ( A  C_  C  ->  ( A  u.  B )  C_  C ) )
2622, 25syl6bi 219 . . . . . . . 8  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  ->  ( A  C_  C  ->  ( A  u.  B ) 
C_  C ) ) )
2721, 26mpi 16 . . . . . . 7  |-  ( ( C  \  A )  =  B  ->  ( A  C_  C  ->  ( A  u.  B )  C_  C ) )
2827com12 27 . . . . . 6  |-  ( A 
C_  C  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  C_  C )
)
2928adantr 451 . . . . 5  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  C_  C )
)
3029imp 418 . . . 4  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  -> 
( A  u.  B
)  C_  C )
31 eqimss 3230 . . . . . . 7  |-  ( ( C  \  A )  =  B  ->  ( C  \  A )  C_  B )
3231adantl 452 . . . . . 6  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  -> 
( C  \  A
)  C_  B )
33 ssundif 3537 . . . . . 6  |-  ( C 
C_  ( A  u.  B )  <->  ( C  \  A )  C_  B
)
3432, 33sylibr 203 . . . . 5  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  ->  C  C_  ( A  u.  B ) )
3534adantlr 695 . . . 4  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  ->  C  C_  ( A  u.  B ) )
3630, 35eqssd 3196 . . 3  |-  ( ( ( A  C_  C  /\  ( A  i^i  B
)  =  (/) )  /\  ( C  \  A )  =  B )  -> 
( A  u.  B
)  =  C )
3736ex 423 . 2  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( C  \  A
)  =  B  -> 
( A  u.  B
)  =  C ) )
3820, 37impbid 183 1  |-  ( ( A  C_  C  /\  ( A  i^i  B )  =  (/) )  ->  (
( A  u.  B
)  =  C  <->  ( C  \  A )  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    \ cdif 3149    u. cun 3150    i^i cin 3151    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  hashbclem  11390  lecldbas  16949  conndisj  17142  ptuncnv  17498  ptunhmeo  17499  cldsubg  17793  icopnfcld  18277  iocmnfcld  18278  voliunlem1  18907  icombl  18921  ioombl  18922  uniioombllem4  18941  ismbf3d  19009  lhop  19363  subfacp1lem3  23713  subfacp1lem5  23715  pconcon  23762  cvmscld  23804
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator