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

Theorem iccssxr 12449
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 12375 . 2 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
21ixxssxr 12380 1 (𝐴[,]𝐵) ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wss 3715  (class class class)co 6813  *cxr 10265  cle 10267  [,]cicc 12371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-1st 7333  df-2nd 7334  df-xr 10270  df-icc 12375
This theorem is referenced by:  xrge0nre  12470  supicclub2  12516  lecldbas  21225  ordtresticc  21229  prdsxmetlem  22374  xrge0gsumle  22837  xrge0tsms  22838  metdscn  22860  iccpnfhmeo  22945  xrhmeo  22946  volsup  23524  volsup2  23573  volivth  23575  itg2le  23705  itg2const2  23707  itg2lea  23710  itg2eqa  23711  itg2split  23715  itg2gt0  23726  dvgt0lem1  23964  radcnvlt1  24371  radcnvle  24373  pserulm  24375  psercnlem2  24377  psercnlem1  24378  psercn  24379  pserdvlem1  24380  pserdvlem2  24381  abelthlem3  24386  abelth  24394  logtayl  24605  xrge0infss  29834  xrge0infssd  29835  xrge0subcld  29837  infxrge0lb  29838  infxrge0glb  29839  infxrge0gelb  29840  xrge0base  29994  xrge00  29995  xrge0mulgnn0  29998  xrge0addass  29999  xrge0addgt0  30000  xrge0adddir  30001  xrge0adddi  30002  xrge0npcan  30003  xrge0omnd  30020  xrge0tsmsd  30094  xrge0slmod  30153  xrge0iifiso  30290  xrge0iifhmeo  30291  xrge0pluscn  30295  xrge0mulc1cn  30296  xrge0tmdOLD  30300  lmlimxrge0  30303  pnfneige0  30306  lmxrge0  30307  esummono  30425  esumpad  30426  esumpad2  30427  esumle  30429  gsumesum  30430  esumlub  30431  esumlef  30433  esumcst  30434  esumrnmpt2  30439  esumfsup  30441  esumpinfval  30444  esumpfinvallem  30445  esumpinfsum  30448  esumpmono  30450  esummulc2  30453  esumdivc  30454  hasheuni  30456  esumcvg  30457  esumgect  30461  esumcvgre  30462  esum2d  30464  measun  30583  measunl  30588  measiun  30590  voliune  30601  volfiniune  30602  ddemeas  30608  omsfval  30665  omsf  30667  oms0  30668  omssubaddlem  30670  omssubadd  30671  baselcarsg  30677  0elcarsg  30678  difelcarsg  30681  inelcarsg  30682  carsgsigalem  30686  carsggect  30689  carsgclctunlem2  30690  carsgclctunlem3  30691  carsgclctun  30692  omsmeas  30694  pmeasmono  30695  probmeasb  30801  mblfinlem1  33759  itg2addnclem  33774  ftc1anc  33806  xadd0ge  40034  xrge0nemnfd  40046  xadd0ge2  40055  eliccxr  40240  ge0lere  40262  inficc  40264  iccdificc  40269  fourierdlem1  40828  fourierdlem20  40847  fourierdlem27  40854  fourierdlem87  40913  fge0iccico  41090  gsumge0cl  41091  sge0sn  41099  sge0tsms  41100  sge0xrcl  41105  sge0pr  41114  sge0prle  41121  sge0le  41127  sge0split  41129  sge0p1  41134  sge0rernmpt  41142  sge0xrclmpt  41148  sge0xadd  41155  meaxrcl  41181  meadjun  41182  voliunsge0lem  41192  caragen0  41226  omexrcl  41227  caragenunidm  41228  caragendifcl  41234  omeunle  41236  omeiunle  41237  carageniuncl  41243  ovn0lem  41285  ovnxrcl  41289  hoidmvlelem3  41317  hoidmvlelem4  41318  vonxrcl  41388
  Copyright terms: Public domain W3C validator