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

Theorem uneqdifeq 3919
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 3644 . . . . 5  |-  ( B  u.  A )  =  ( A  u.  B
)
2 eqtr 2483 . . . . . . 7  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  ( B  u.  A )  =  C )
32eqcomd 2465 . . . . . 6  |-  ( ( ( B  u.  A
)  =  ( A  u.  B )  /\  ( A  u.  B
)  =  C )  ->  C  =  ( B  u.  A ) )
4 difeq1 3611 . . . . . . 7  |-  ( C  =  ( B  u.  A )  ->  ( C  \  A )  =  ( ( B  u.  A )  \  A
) )
5 difun2 3910 . . . . . . 7  |-  ( ( B  u.  A ) 
\  A )  =  ( B  \  A
)
6 eqtr 2483 . . . . . . . 8  |-  ( ( ( C  \  A
)  =  ( ( B  u.  A ) 
\  A )  /\  ( ( B  u.  A )  \  A
)  =  ( B 
\  A ) )  ->  ( C  \  A )  =  ( B  \  A ) )
7 incom 3687 . . . . . . . . . . 11  |-  ( A  i^i  B )  =  ( B  i^i  A
)
87eqeq1i 2464 . . . . . . . . . 10  |-  ( ( A  i^i  B )  =  (/)  <->  ( B  i^i  A )  =  (/) )
9 disj3 3874 . . . . . . . . . 10  |-  ( ( B  i^i  A )  =  (/)  <->  B  =  ( B  \  A ) )
108, 9bitri 249 . . . . . . . . 9  |-  ( ( A  i^i  B )  =  (/)  <->  B  =  ( B  \  A ) )
11 eqtr 2483 . . . . . . . . . . 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 2469 . . . . . . . . 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 3627 . . . . . . . 8  |-  ( C 
\  A )  C_  C
22 sseq1 3520 . . . . . . . . 9  |-  ( ( C  \  A )  =  B  ->  (
( C  \  A
)  C_  C  <->  B  C_  C
) )
23 unss 3674 . . . . . . . . . . 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 3551 . . . . . . 7  |-  ( ( C  \  A )  =  B  ->  ( C  \  A )  C_  B )
3231adantl 466 . . . . . 6  |-  ( ( A  C_  C  /\  ( C  \  A )  =  B )  -> 
( C  \  A
)  C_  B )
33 ssundif 3914 . . . . . 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 3516 . . 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 1395    \ cdif 3468    u. cun 3469    i^i cin 3470    C_ wss 3471   (/)c0 3793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794
This theorem is referenced by:  fzdifsuc  11765  hashbclem  12505  lecldbas  19847  conndisj  20043  ptuncnv  20434  ptunhmeo  20435  cldsubg  20735  icopnfcld  21401  iocmnfcld  21402  voliunlem1  22086  icombl  22100  ioombl  22101  uniioombllem4  22121  ismbf3d  22187  lhop  22543  subfacp1lem3  28823  subfacp1lem5  28825  pconcon  28873  cvmscld  28915
  Copyright terms: Public domain W3C validator