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

Theorem iccssxr 12811
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 12737 . 2 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
21ixxssxr 12742 1 (𝐴[,]𝐵) ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wss 3934  (class class class)co 7148  *cxr 10666  cle 10668  [,]cicc 12733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-1st 7681  df-2nd 7682  df-xr 10671  df-icc 12737
This theorem is referenced by:  eliccxr  12815  supicclub2  12881  lecldbas  21819  ordtresticc  21823  prdsxmetlem  22970  xrge0gsumle  23433  xrge0tsms  23434  metdscn  23456  iccpnfhmeo  23541  xrhmeo  23542  volsup  24149  volsup2  24198  volivth  24200  itg2le  24332  itg2const2  24334  itg2lea  24337  itg2eqa  24338  itg2split  24342  itg2gt0  24353  dvgt0lem1  24591  radcnvlt1  24998  radcnvle  25000  pserulm  25002  psercnlem2  25004  psercnlem1  25005  psercn  25006  pserdvlem1  25007  pserdvlem2  25008  abelthlem3  25013  abelth  25021  logtayl  25235  xrge0infss  30476  xrge0infssd  30477  xrge0subcld  30479  infxrge0lb  30480  infxrge0glb  30481  infxrge0gelb  30482  xrge0base  30665  xrge00  30666  xrge0mulgnn0  30669  xrge0addass  30670  xrge0addgt0  30671  xrge0adddir  30672  xrge0adddi  30673  xrge0npcan  30674  xrge0tsmsd  30685  xrge0slmod  30910  xrge0iifiso  31166  xrge0iifhmeo  31167  xrge0pluscn  31171  xrge0mulc1cn  31172  xrge0tmdALT  31177  lmlimxrge0  31179  pnfneige0  31182  lmxrge0  31183  esummono  31301  esumpad  31302  esumpad2  31303  esumle  31305  gsumesum  31306  esumlub  31307  esumlef  31309  esumcst  31310  esumrnmpt2  31315  esumfsup  31317  esumpinfval  31320  esumpfinvallem  31321  esumpinfsum  31324  esumpmono  31326  esummulc2  31329  esumdivc  31330  hasheuni  31332  esumcvg  31333  esumgect  31337  esum2d  31340  measun  31458  measunl  31463  measiun  31465  voliune  31476  volfiniune  31477  ddemeas  31483  omsfval  31540  omsf  31542  oms0  31543  omssubaddlem  31545  omssubadd  31546  baselcarsg  31552  0elcarsg  31553  difelcarsg  31556  inelcarsg  31557  carsgsigalem  31561  carsggect  31564  carsgclctunlem2  31565  carsgclctunlem3  31566  carsgclctun  31567  omsmeas  31569  pmeasmono  31570  probmeasb  31676  itg2addnclem  34925  ftc1anc  34957  xadd0ge  41567  xrge0nemnfd  41579  xadd0ge2  41588  ge0lere  41787  inficc  41789  iccdificc  41794  fourierdlem1  42373  fourierdlem20  42392  fourierdlem27  42399  fourierdlem87  42458  fge0iccico  42632  gsumge0cl  42633  sge0sn  42641  sge0tsms  42642  sge0xrcl  42647  sge0pr  42656  sge0prle  42663  sge0le  42669  sge0split  42671  sge0p1  42676  sge0rernmpt  42684  sge0xrclmpt  42690  sge0xadd  42697  meaxrcl  42723  meadjun  42724  voliunsge0lem  42734  caragen0  42768  omexrcl  42769  caragenunidm  42770  caragendifcl  42776  omeunle  42778  omeiunle  42779  carageniuncl  42785  ovn0lem  42827  ovnxrcl  42831  hoidmvlelem3  42859  hoidmvlelem4  42860  vonxrcl  42930
  Copyright terms: Public domain W3C validator