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

Theorem ixxun 11659
Description: Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014.)
Hypotheses
Ref Expression
ixx.1  |-  O  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x R z  /\  z S y ) } )
ixxun.2  |-  P  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x T z  /\  z U y ) } )
ixxun.3  |-  ( ( B  e.  RR*  /\  w  e.  RR* )  ->  ( B T w  <->  -.  w S B ) )
ixxun.4  |-  Q  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x R z  /\  z U y ) } )
ixxun.5  |-  ( ( w  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( w S B  /\  B X C )  ->  w U C ) )
ixxun.6  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  ->  (
( A W B  /\  B T w )  ->  A R w ) )
Assertion
Ref Expression
ixxun  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( ( A O B )  u.  ( B P C ) )  =  ( A Q C ) )
Distinct variable groups:    x, w, y, z, A    w, C, x, y, z    w, O   
w, Q    w, B, x, y, z    w, P   
x, R, y, z   
x, S, y, z   
x, T, y, z   
x, U, y, z   
w, W    w, X
Allowed substitution hints:    P( x, y, z)    Q( x, y, z)    R( w)    S( w)    T( w)    U( w)    O( x, y, z)    W( x, y, z)    X( x, y, z)

Proof of Theorem ixxun
StepHypRef Expression
1 elun 3606 . . 3  |-  ( w  e.  ( ( A O B )  u.  ( B P C ) )  <->  ( w  e.  ( A O B )  \/  w  e.  ( B P C ) ) )
2 simpl1 1008 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  ->  A  e.  RR* )
3 simpl2 1009 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  ->  B  e.  RR* )
4 ixx.1 . . . . . . . . . . 11  |-  O  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x R z  /\  z S y ) } )
54elixx1 11652 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
w  e.  ( A O B )  <->  ( w  e.  RR*  /\  A R w  /\  w S B ) ) )
62, 3, 5syl2anc 665 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( w  e.  ( A O B )  <-> 
( w  e.  RR*  /\  A R w  /\  w S B ) ) )
76biimpa 486 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  -> 
( w  e.  RR*  /\  A R w  /\  w S B ) )
87simp1d 1017 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  ->  w  e.  RR* )
97simp2d 1018 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  ->  A R w )
107simp3d 1019 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  ->  w S B )
11 simplrr 769 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  ->  B X C )
123adantr 466 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  ->  B  e.  RR* )
13 simpl3 1010 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  ->  C  e.  RR* )
1413adantr 466 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  ->  C  e.  RR* )
15 ixxun.5 . . . . . . . . 9  |-  ( ( w  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( w S B  /\  B X C )  ->  w U C ) )
168, 12, 14, 15syl3anc 1264 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  -> 
( ( w S B  /\  B X C )  ->  w U C ) )
1710, 11, 16mp2and 683 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  ->  w U C )
188, 9, 173jca 1185 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A O B ) )  -> 
( w  e.  RR*  /\  A R w  /\  w U C ) )
19 ixxun.2 . . . . . . . . . . 11  |-  P  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x T z  /\  z U y ) } )
2019elixx1 11652 . . . . . . . . . 10  |-  ( ( B  e.  RR*  /\  C  e.  RR* )  ->  (
w  e.  ( B P C )  <->  ( w  e.  RR*  /\  B T w  /\  w U C ) ) )
213, 13, 20syl2anc 665 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( w  e.  ( B P C )  <-> 
( w  e.  RR*  /\  B T w  /\  w U C ) ) )
2221biimpa 486 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  -> 
( w  e.  RR*  /\  B T w  /\  w U C ) )
2322simp1d 1017 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  ->  w  e.  RR* )
24 simplrl 768 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  ->  A W B )
2522simp2d 1018 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  ->  B T w )
262adantr 466 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  ->  A  e.  RR* )
273adantr 466 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  ->  B  e.  RR* )
28 ixxun.6 . . . . . . . . 9  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  ->  (
( A W B  /\  B T w )  ->  A R w ) )
2926, 27, 23, 28syl3anc 1264 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  -> 
( ( A W B  /\  B T w )  ->  A R w ) )
3024, 25, 29mp2and 683 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  ->  A R w )
3122simp3d 1019 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  ->  w U C )
3223, 30, 313jca 1185 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( B P C ) )  -> 
( w  e.  RR*  /\  A R w  /\  w U C ) )
3318, 32jaodan 792 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  ( w  e.  ( A O B )  \/  w  e.  ( B P C ) ) )  ->  ( w  e.  RR*  /\  A R w  /\  w U C ) )
34 ixxun.4 . . . . . . . 8  |-  Q  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x R z  /\  z U y ) } )
3534elixx1 11652 . . . . . . 7  |-  ( ( A  e.  RR*  /\  C  e.  RR* )  ->  (
w  e.  ( A Q C )  <->  ( w  e.  RR*  /\  A R w  /\  w U C ) ) )
362, 13, 35syl2anc 665 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( w  e.  ( A Q C )  <-> 
( w  e.  RR*  /\  A R w  /\  w U C ) ) )
3736biimpar 487 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  ( w  e.  RR*  /\  A R w  /\  w U C ) )  ->  w  e.  ( A Q C ) )
3833, 37syldan 472 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  ( w  e.  ( A O B )  \/  w  e.  ( B P C ) ) )  ->  w  e.  ( A Q C ) )
39 exmid 416 . . . . 5  |-  ( w S B  \/  -.  w S B )
40 df-3an 984 . . . . . . . . 9  |-  ( ( w  e.  RR*  /\  A R w  /\  w S B )  <->  ( (
w  e.  RR*  /\  A R w )  /\  w S B ) )
416, 40syl6bb 264 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( w  e.  ( A O B )  <-> 
( ( w  e. 
RR*  /\  A R w )  /\  w S B ) ) )
4241adantr 466 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w  e.  ( A O B )  <-> 
( ( w  e. 
RR*  /\  A R w )  /\  w S B ) ) )
4336biimpa 486 . . . . . . . . . 10  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w  e.  RR*  /\  A R w  /\  w U C ) )
4443simp1d 1017 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  ->  w  e.  RR* )
4543simp2d 1018 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  ->  A R w )
4644, 45jca 534 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w  e.  RR*  /\  A R w ) )
4746biantrurd 510 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w S B  <-> 
( ( w  e. 
RR*  /\  A R w )  /\  w S B ) ) )
4842, 47bitr4d 259 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w  e.  ( A O B )  <-> 
w S B ) )
49 3anan12 995 . . . . . . . . 9  |-  ( ( w  e.  RR*  /\  B T w  /\  w U C )  <->  ( B T w  /\  (
w  e.  RR*  /\  w U C ) ) )
5021, 49syl6bb 264 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( w  e.  ( B P C )  <-> 
( B T w  /\  ( w  e. 
RR*  /\  w U C ) ) ) )
5150adantr 466 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w  e.  ( B P C )  <-> 
( B T w  /\  ( w  e. 
RR*  /\  w U C ) ) ) )
5243simp3d 1019 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  ->  w U C )
5344, 52jca 534 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w  e.  RR*  /\  w U C ) )
5453biantrud 509 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( B T w  <-> 
( B T w  /\  ( w  e. 
RR*  /\  w U C ) ) ) )
553adantr 466 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  ->  B  e.  RR* )
56 ixxun.3 . . . . . . . 8  |-  ( ( B  e.  RR*  /\  w  e.  RR* )  ->  ( B T w  <->  -.  w S B ) )
5755, 44, 56syl2anc 665 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( B T w  <->  -.  w S B ) )
5851, 54, 573bitr2d 284 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w  e.  ( B P C )  <->  -.  w S B ) )
5948, 58orbi12d 714 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( ( w  e.  ( A O B )  \/  w  e.  ( B P C ) )  <->  ( w S B  \/  -.  w S B ) ) )
6039, 59mpbiri 236 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  /\  w  e.  ( A Q C ) )  -> 
( w  e.  ( A O B )  \/  w  e.  ( B P C ) ) )
6138, 60impbida 840 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( ( w  e.  ( A O B )  \/  w  e.  ( B P C ) )  <->  w  e.  ( A Q C ) ) )
621, 61syl5bb 260 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( w  e.  ( ( A O B )  u.  ( B P C ) )  <-> 
w  e.  ( A Q C ) ) )
6362eqrdv 2419 1  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A W B  /\  B X C ) )  -> 
( ( A O B )  u.  ( B P C ) )  =  ( A Q C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   {crab 2775    u. cun 3434   class class class wbr 4423  (class class class)co 6306    |-> cmpt2 6308   RR*cxr 9682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-iota 5565  df-fun 5603  df-fv 5609  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-xr 9687
This theorem is referenced by:  icoun  11764  snunioo  11766  snunico  11767  snunioc  11768  ioojoin  11771  leordtval2  20227  lecldbas  20234  icopnfcld  21787  iocmnfcld  21788  ioombl  22517  ismbf3d  22609  joiniooico  28363  asindmre  31992  ioounsn  36065  snunioo2  37556  snunioo1  37563
  Copyright terms: Public domain W3C validator