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

Theorem iccssxr 12198
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 12124 . 2 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
21ixxssxr 12129 1 (𝐴[,]𝐵) ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wss 3555  (class class class)co 6604  *cxr 10017  cle 10019  [,]cicc 12120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-1st 7113  df-2nd 7114  df-xr 10022  df-icc 12124
This theorem is referenced by:  xrge0nre  12219  supicclub2  12265  lecldbas  20933  ordtresticc  20937  prdsxmetlem  22083  xrge0gsumle  22544  xrge0tsms  22545  metdscn  22567  iccpnfhmeo  22652  xrhmeo  22653  volsup  23231  volsup2  23279  volivth  23281  itg2le  23412  itg2const2  23414  itg2lea  23417  itg2eqa  23418  itg2split  23422  itg2gt0  23433  dvgt0lem1  23669  radcnvlt1  24076  radcnvle  24078  pserulm  24080  psercnlem2  24082  psercnlem1  24083  psercn  24084  pserdvlem1  24085  pserdvlem2  24086  abelthlem3  24091  abelth  24099  logtayl  24306  xrge0infss  29366  xrge0infssd  29367  xrge0subcld  29369  infxrge0lb  29370  infxrge0glb  29371  infxrge0gelb  29372  xrge0base  29467  xrge00  29468  xrge0mulgnn0  29471  xrge0addass  29472  xrge0addgt0  29473  xrge0adddir  29474  xrge0adddi  29475  xrge0npcan  29476  xrge0omnd  29493  xrge0tsmsd  29567  xrge0slmod  29626  xrge0iifiso  29760  xrge0iifhmeo  29761  xrge0pluscn  29765  xrge0mulc1cn  29766  xrge0tmdOLD  29770  lmlimxrge0  29773  pnfneige0  29776  lmxrge0  29777  esummono  29894  esumpad  29895  esumpad2  29896  esumle  29898  gsumesum  29899  esumlub  29900  esumlef  29902  esumcst  29903  esumrnmpt2  29908  esumfsup  29910  esumpinfval  29913  esumpfinvallem  29914  esumpinfsum  29917  esumpmono  29919  esummulc2  29922  esumdivc  29923  hasheuni  29925  esumcvg  29926  esumgect  29930  esumcvgre  29931  esum2d  29933  measun  30052  measunl  30057  measiun  30059  voliune  30070  volfiniune  30071  ddemeas  30077  omsfval  30134  omsf  30136  oms0  30137  omssubaddlem  30139  omssubadd  30140  baselcarsg  30146  0elcarsg  30147  difelcarsg  30150  inelcarsg  30151  carsgsigalem  30155  carsggect  30158  carsgclctunlem2  30159  carsgclctunlem3  30160  carsgclctun  30161  omsmeas  30163  pmeasmono  30164  probmeasb  30270  mblfinlem1  33075  itg2addnclem  33090  ftc1anc  33122  xadd0ge  38997  xrge0nemnfd  39009  xadd0ge2  39018  eliccxr  39145  ge0lere  39167  inficc  39169  iccdificc  39174  fourierdlem1  39629  fourierdlem20  39648  fourierdlem27  39655  fourierdlem87  39714  fge0iccico  39891  gsumge0cl  39892  sge0sn  39900  sge0tsms  39901  sge0xrcl  39906  sge0pr  39915  sge0prle  39922  sge0le  39928  sge0split  39930  sge0p1  39935  sge0rernmpt  39943  sge0xrclmpt  39949  sge0xadd  39956  meaxrcl  39982  meadjun  39983  voliunsge0lem  39993  caragen0  40024  omexrcl  40025  caragenunidm  40026  caragendifcl  40032  omeunle  40034  omeiunle  40035  carageniuncl  40041  ovn0lem  40083  ovnxrcl  40087  hoidmvlelem3  40115  hoidmvlelem4  40116  vonxrcl  40186
  Copyright terms: Public domain W3C validator