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

Theorem iccssxr 12127
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 (𝐴[,]𝐵) ⊆ ℝ*

Proof of Theorem iccssxr
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-icc 12053 . 2 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
21ixxssxr 12058 1 (𝐴[,]𝐵) ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wss 3540  (class class class)co 6549  *cxr 9952  cle 9954  [,]cicc 12049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-xr 9957  df-icc 12053
This theorem is referenced by:  xrge0nre  12148  supicclub2  12194  lecldbas  20833  ordtresticc  20837  prdsxmetlem  21983  xrge0gsumle  22444  xrge0tsms  22445  metdscn  22467  iccpnfhmeo  22552  xrhmeo  22553  volsup  23131  volsup2  23179  volivth  23181  itg2le  23312  itg2const2  23314  itg2lea  23317  itg2eqa  23318  itg2split  23322  itg2gt0  23333  dvgt0lem1  23569  radcnvlt1  23976  radcnvle  23978  pserulm  23980  psercnlem2  23982  psercnlem1  23983  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  abelthlem3  23991  abelth  23999  logtayl  24206  xrge0infss  28915  xrge0infssd  28916  xrge0subcld  28918  infxrge0lb  28919  infxrge0glb  28920  infxrge0gelb  28921  xrge0base  29016  xrge00  29017  xrge0mulgnn0  29020  xrge0addass  29021  xrge0addgt0  29022  xrge0adddir  29023  xrge0adddi  29024  xrge0npcan  29025  xrge0omnd  29042  xrge0tsmsd  29116  xrge0slmod  29175  xrge0iifiso  29309  xrge0iifhmeo  29310  xrge0pluscn  29314  xrge0mulc1cn  29315  xrge0tmdOLD  29319  lmlimxrge0  29322  pnfneige0  29325  lmxrge0  29326  esummono  29443  esumpad  29444  esumpad2  29445  esumle  29447  gsumesum  29448  esumlub  29449  esumlef  29451  esumcst  29452  esumrnmpt2  29457  esumfsup  29459  esumpinfval  29462  esumpfinvallem  29463  esumpinfsum  29466  esumpmono  29468  esummulc2  29471  esumdivc  29472  hasheuni  29474  esumcvg  29475  esumgect  29479  esumcvgre  29480  esum2d  29482  measun  29601  measunl  29606  measiun  29608  voliune  29619  volfiniune  29620  ddemeas  29626  omsfval  29683  omsf  29685  oms0  29686  omssubaddlem  29688  omssubadd  29689  baselcarsg  29695  0elcarsg  29696  difelcarsg  29699  inelcarsg  29700  carsgsigalem  29704  carsggect  29707  carsgclctunlem2  29708  carsgclctunlem3  29709  carsgclctun  29710  omsmeas  29712  pmeasmono  29713  probmeasb  29819  mblfinlem1  32616  itg2addnclem  32631  ftc1anc  32663  xadd0ge  38477  xrge0nemnfd  38489  xadd0ge2  38498  eliccxr  38584  ge0lere  38606  inficc  38608  iccdificc  38613  fourierdlem1  39001  fourierdlem20  39020  fourierdlem27  39027  fourierdlem87  39086  fge0iccico  39263  gsumge0cl  39264  sge0sn  39272  sge0tsms  39273  sge0xrcl  39278  sge0pr  39287  sge0prle  39294  sge0le  39300  sge0split  39302  sge0p1  39307  sge0rernmpt  39315  sge0xrclmpt  39321  sge0xadd  39328  meaxrcl  39354  meadjun  39355  voliunsge0lem  39365  caragen0  39396  omexrcl  39397  caragenunidm  39398  caragendifcl  39404  omeunle  39406  omeiunle  39407  carageniuncl  39413  ovn0lem  39455  ovnxrcl  39459  hoidmvlelem3  39487  hoidmvlelem4  39488  vonxrcl  39558
  Copyright terms: Public domain W3C validator