MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ixxun Structured version   Visualization version   Unicode version
Theorem ixxun 12191
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 3753 . . 3 |- ( w e. ( ( A O B ) u. ( B P C ) ) <-> ( w e. ( A O B ) \/ w e. ( B P C ) ) )
2 simpl1 1064 . . . . . . . . . 10 |- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> A e. RR* )
3 simpl2 1065 . . . . . . . . . 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 12184 . . . . . . . . . 10 |- ( ( A e. RR* /\ B e. RR* ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
62, 3, 5syl2anc 693 . . . . . . . . 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 501 . . . . . . . 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 1073 . . . . . . 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 1074 . . . . . . 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 1075 . . . . . . . 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 801 . . . . . . . 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 481 . . . . . . . . 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 1066 . . . . . . . . . 10 |- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> C e. RR* )
1413adantr 481 . . . . . . . . 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 1326 . . . . . . . 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 715 . . . . . . 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 1242 . . . . . 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 12184 . . . . . . . . . 10 |- ( ( B e. RR* /\ C e. RR* ) -> ( w e. ( B P C ) <-> ( w e. RR* /\ B T w /\ w U C ) ) )
213, 13, 20syl2anc 693 . . . . . . . . 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 501 . . . . . . . 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 1073 . . . . . . 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 800 . . . . . . . 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 1074 . . . . . . . 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 481 . . . . . . . . 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 481 . . . . . . . . 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 1326 . . . . . . . 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 715 . . . . . . 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 1075 . . . . . . 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 1242 . . . . . 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 826 . . . . 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 12184 . . . . . . 7 |- ( ( A e. RR* /\ C e. RR* ) -> ( w e. ( A Q C ) <-> ( w e. RR* /\ A R w /\ w U C ) ) )
362, 13, 35syl2anc 693 . . . . . 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 502 . . . . 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 487 . . . 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 431 . . . . 5 |- ( w S B \/ -. w S B )
40 df-3an 1039 . . . . . . . . 9 |- ( ( w e. RR* /\ A R w /\ w S B ) <-> ( ( w e. RR* /\ A R w ) /\ w S B ) )
416, 40syl6bb 276 . . . . . . . 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 481 . . . . . . 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 501 . . . . . . . . . 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 1073 . . . . . . . . 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 1074 . . . . . . . . 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 554 . . . . . . . 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 529 . . . . . . 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 271 . . . . . 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 1051 . . . . . . . . 9 |- ( ( w e. RR* /\ B T w /\ w U C ) <-> ( B T w /\ ( w e. RR* /\ w U C ) ) )
5021, 49syl6bb 276 . . . . . . . 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 481 . . . . . . 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 1075 . . . . . . . . 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 554 . . . . . . . 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 528 . . . . . . 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 481 . . . . . . . 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 693 . . . . . . 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 296 . . . . . 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 746 . . . . 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 248 . . . 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 877 . . 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 272 . 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 2620 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 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {crab 2916   u. cun 3572   class class class wbr 4653  (class class class)co 6650   |-> cmpt2 6652   RR*cxr 10073
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-xr 10078
This theorem is referenced by:  icoun  12296  snunioo  12298  snunico  12299  snunioc  12300  ioojoin  12303  leordtval2  21016  lecldbas  21023  icopnfcld  22571  iocmnfcld  22572  ioombl  23333  ismbf3d  23421  joiniooico  29536  asindmre  33495  ioounsn  37795  snunioo2  39731  snunioo1  39738
  Copyright terms: Public domain W3C validator