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

Theorem iccssxr 11659
Description: A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
Assertion
Ref Expression
iccssxr  |-  ( A [,] B )  C_  RR*

Proof of Theorem iccssxr
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-icc 11588 . 2  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
21ixxssxr 11593 1  |-  ( A [,] B )  C_  RR*
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3413  (class class class)co 6277   RR*cxr 9656    <_ cle 9658   [,]cicc 11584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-cnex 9577  ax-resscn 9578
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-fv 5576  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-1st 6783  df-2nd 6784  df-xr 9661  df-icc 11588
This theorem is referenced by:  supicclub2  11723  lecldbas  20011  ordtresticc  20015  prdsxmetlem  21161  xrge0gsumle  21628  xrge0tsms  21629  metdscn  21650  iccpnfhmeo  21735  xrhmeo  21736  volsup  22256  volsup2  22304  volivth  22306  itg2le  22436  itg2const2  22438  itg2lea  22441  itg2eqa  22442  itg2split  22446  itg2gt0  22457  dvgt0lem1  22693  radcnvlt1  23103  radcnvle  23105  pserulm  23107  psercnlem2  23109  psercnlem1  23110  psercn  23111  pserdvlem1  23112  pserdvlem2  23113  abelthlem3  23118  abelth  23126  logtayl  23333  xrge0infss  28008  xrge0infssd  28009  xrge0subcld  28011  infxrge0lb  28012  infxrge0glb  28013  infxrge0gelb  28014  xrge0base  28111  xrge00  28112  xrge0mulgnn0  28115  xrge0addass  28116  xrge0nre  28118  xrge0addgt0  28119  xrge0adddir  28120  xrge0adddi  28121  xrge0npcan  28122  xrge0omnd  28139  xrge0tsmsd  28214  xrge0slmod  28273  xrge0iifiso  28356  xrge0iifhmeo  28357  xrge0pluscn  28361  xrge0mulc1cn  28362  xrge0tmdOLD  28366  lmlimxrge0  28369  pnfneige0  28372  lmxrge0  28373  esummono  28487  esumpad  28488  esumpad2  28489  esumle  28491  gsumesum  28492  esumlub  28493  esumlef  28495  esumcst  28496  esumrnmpt2  28501  esumfsup  28503  esumpinfval  28506  esumpfinvallem  28507  esumpinfsum  28510  esumpmono  28512  esummulc2  28515  esumdivc  28516  hasheuni  28518  esumcvg  28519  esumgect  28523  esumcvgre  28524  esum2d  28526  measun  28645  measunl  28650  measiun  28652  voliune  28664  volfiniune  28665  ddemeas  28671  omsfval  28728  omsf  28730  oms0  28731  omssubaddlem  28733  omssubadd  28734  baselcarsg  28740  0elcarsg  28741  difelcarsg  28744  inelcarsg  28745  carsgsigalem  28749  carsggect  28752  carsgclctunlem2  28753  carsgclctunlem3  28754  carsgclctun  28755  omsmeas  28757  pmeasmono  28758  probmeasb  28861  mblfinlem1  31403  itg2addnclem  31419  ftc1anc  31451  eliccxr  36899  fourierdlem1  37239  fourierdlem20  37258  fourierdlem27  37265  fourierdlem87  37325
  Copyright terms: Public domain W3C validator