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

Theorem iooss1 11327
Description: Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
Assertion
Ref Expression
iooss1  |-  ( ( A  e.  RR*  /\  A  <_  B )  ->  ( B (,) C )  C_  ( A (,) C ) )

Proof of Theorem iooss1
Dummy variables  x  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ioo 11296 . 2  |-  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) } )
2 xrlelttr 11122 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  ->  (
( A  <_  B  /\  B  <  w )  ->  A  <  w
) )
31, 1, 2ixxss1 11310 1  |-  ( ( A  e.  RR*  /\  A  <_  B )  ->  ( B (,) C )  C_  ( A (,) C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756    C_ wss 3321   class class class wbr 4285  (class class class)co 6086   RR*cxr 9409    < clt 9410    <_ cle 9411   (,)cioo 11292
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-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-pre-lttri 9348  ax-pre-lttrn 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-po 4633  df-so 4634  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-1st 6572  df-2nd 6573  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-ioo 11296
This theorem is referenced by:  ioodisj  11407  tgqioo  20346  ioorcl2  21021  itg2gt0  21207  itgsplitioo  21284  ditgcl  21302  ditgswap  21303  ditgsplitlem  21304  dvferm1lem  21425  dvferm  21429  dvlip  21434  dvgt0lem1  21443  dvivthlem1  21449  lhop1lem  21454  lhop2  21456  dvcvx  21461  dvfsumle  21462  dvfsumge  21463  dvfsumabs  21464  ftc1lem1  21476  ftc1a  21478  ftc1lem4  21480  ftc2ditglem  21486  tanregt0  21964  basellem4  22390  pntlemp  22828
  Copyright terms: Public domain W3C validator