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

Theorem ioossicc 11601
Description: An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
Assertion
Ref Expression
ioossicc  |-  ( A (,) B )  C_  ( A [,] B )

Proof of Theorem ioossicc
Dummy variables  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ioo 11524 . 2  |-  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) } )
2 df-icc 11527 . 2  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
3 xrltle 11346 . 2  |-  ( ( A  e.  RR*  /\  w  e.  RR* )  ->  ( A  <  w  ->  A  <_  w ) )
4 xrltle 11346 . 2  |-  ( ( w  e.  RR*  /\  B  e.  RR* )  ->  (
w  <  B  ->  w  <_  B ) )
51, 2, 3, 4ixxssixx 11534 1  |-  ( A (,) B )  C_  ( A [,] B )
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3471  (class class class)co 6277    < clt 9619    <_ cle 9620   (,)cioo 11520   [,]cicc 11523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569  ax-cnex 9539  ax-resscn 9540  ax-pre-lttri 9557  ax-pre-lttrn 9558
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-nel 2660  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-mpt 4502  df-id 4790  df-po 4795  df-so 4796  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-er 7303  df-en 7509  df-dom 7510  df-sdom 7511  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-ioo 11524  df-icc 11527
This theorem is referenced by:  ioodisj  11641  iccntr  21056  ivth2  21597  ivthle  21598  ivthle2  21599  ovolioo  21708  uniiccvol  21719  itgioo  21952  rollelem  22120  rolle  22121  cmvth  22122  dvlip  22124  dvlipcn  22125  dvlip2  22126  c1liplem1  22127  dvle  22138  dvivthlem1  22139  dvne0  22142  lhop1lem  22144  dvcnvrelem1  22148  dvfsumle  22152  dvfsumge  22153  dvfsumabs  22154  dvfsumlem2  22158  ftc1a  22168  ftc1lem4  22170  ftc1lem5  22171  ftc1lem6  22172  ftc1  22173  ftc2  22175  itgparts  22178  itgsubstlem  22179  itgsubst  22180  reeff1olem  22570  efcvx  22573  tanord1  22652  logccv  22767  loglesqr  22855  chordthm  22891  amgmlem  23042  eliccioo  27283  xrge0mulc1cn  27547  lgamgulmlem2  28200  itg2gt0cn  29636  ftc1cnnclem  29654  ftc1cnnc  29655  ftc2nc  29665  areacirc  29678  ivthALT  29719  itgpowd  30778  lhe4.4ex1a  30791  limciccioolb  31120  limcicciooub  31136  icccncfext  31183  cncfiooicclem1  31189  cncfioobdlem  31192  cncfioobd  31193  itgsin0pilem1  31224  iblioosinexp  31227  itgsinexplem1  31228  itgsinexp  31229  ditgeqiooicc  31235  itgcoscmulx  31244  ibliooicc  31246  itgsincmulx  31249  itgsubsticclem  31250  itgioocnicc  31252  iblcncfioo  31253  itgsbtaddcnst  31257  dirkeritg  31359  fourierdlem20  31384  fourierdlem38  31402  fourierdlem39  31403  fourierdlem46  31410  fourierdlem62  31426  fourierdlem68  31432  fourierdlem69  31433  fourierdlem70  31434  fourierdlem72  31436  fourierdlem73  31437  fourierdlem74  31438  fourierdlem75  31439  fourierdlem76  31440  fourierdlem80  31444  fourierdlem81  31445  fourierdlem82  31446  fourierdlem83  31447  fourierdlem84  31448  fourierdlem85  31449  fourierdlem88  31452  fourierdlem92  31456  fourierdlem93  31457  fourierdlem100  31464  fourierdlem101  31465  fourierdlem103  31467  fourierdlem104  31468  fourierdlem107  31471  fourierdlem111  31475  fourierdlem112  31476  sqwvfoura  31486  sqwvfourb  31487  chordthmALT  32690
  Copyright terms: Public domain W3C validator