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

Theorem iccssxr 12505
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 12431 . 2 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
21ixxssxr 12436 1 (𝐴[,]𝐵) ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wss 3769  (class class class)co 6878  *cxr 10362  cle 10364  [,]cicc 12427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-un 7183  ax-cnex 10280  ax-resscn 10281
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-iun 4712  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109  df-ov 6881  df-oprab 6882  df-mpt2 6883  df-1st 7401  df-2nd 7402  df-xr 10367  df-icc 12431
This theorem is referenced by:  eliccxr  12509  supicclub2  12577  lecldbas  21352  ordtresticc  21356  prdsxmetlem  22501  xrge0gsumle  22964  xrge0tsms  22965  metdscn  22987  iccpnfhmeo  23072  xrhmeo  23073  volsup  23664  volsup2  23713  volivth  23715  itg2le  23847  itg2const2  23849  itg2lea  23852  itg2eqa  23853  itg2split  23857  itg2gt0  23868  dvgt0lem1  24106  radcnvlt1  24513  radcnvle  24515  pserulm  24517  psercnlem2  24519  psercnlem1  24520  psercn  24521  pserdvlem1  24522  pserdvlem2  24523  abelthlem3  24528  abelth  24536  logtayl  24747  xrge0infss  30043  xrge0infssd  30044  xrge0subcld  30046  infxrge0lb  30047  infxrge0glb  30048  infxrge0gelb  30049  xrge0base  30201  xrge00  30202  xrge0mulgnn0  30205  xrge0addass  30206  xrge0addgt0  30207  xrge0adddir  30208  xrge0adddi  30209  xrge0npcan  30210  xrge0tsmsd  30301  xrge0slmod  30360  xrge0iifiso  30497  xrge0iifhmeo  30498  xrge0pluscn  30502  xrge0mulc1cn  30503  xrge0tmdOLD  30507  lmlimxrge0  30510  pnfneige0  30513  lmxrge0  30514  esummono  30632  esumpad  30633  esumpad2  30634  esumle  30636  gsumesum  30637  esumlub  30638  esumlef  30640  esumcst  30641  esumrnmpt2  30646  esumfsup  30648  esumpinfval  30651  esumpfinvallem  30652  esumpinfsum  30655  esumpmono  30657  esummulc2  30660  esumdivc  30661  hasheuni  30663  esumcvg  30664  esumgect  30668  esum2d  30671  measun  30790  measunl  30795  measiun  30797  voliune  30808  volfiniune  30809  ddemeas  30815  omsfval  30872  omsf  30874  oms0  30875  omssubaddlem  30877  omssubadd  30878  baselcarsg  30884  0elcarsg  30885  difelcarsg  30888  inelcarsg  30889  carsgsigalem  30893  carsggect  30896  carsgclctunlem2  30897  carsgclctunlem3  30898  carsgclctun  30899  omsmeas  30901  pmeasmono  30902  probmeasb  31009  itg2addnclem  33949  ftc1anc  33981  xadd0ge  40280  xrge0nemnfd  40292  xadd0ge2  40301  ge0lere  40503  inficc  40505  iccdificc  40510  fourierdlem1  41068  fourierdlem20  41087  fourierdlem27  41094  fourierdlem87  41153  fge0iccico  41330  gsumge0cl  41331  sge0sn  41339  sge0tsms  41340  sge0xrcl  41345  sge0pr  41354  sge0prle  41361  sge0le  41367  sge0split  41369  sge0p1  41374  sge0rernmpt  41382  sge0xrclmpt  41388  sge0xadd  41395  meaxrcl  41421  meadjun  41422  voliunsge0lem  41432  caragen0  41466  omexrcl  41467  caragenunidm  41468  caragendifcl  41474  omeunle  41476  omeiunle  41477  carageniuncl  41483  ovn0lem  41525  ovnxrcl  41529  hoidmvlelem3  41557  hoidmvlelem4  41558  vonxrcl  41628
  Copyright terms: Public domain W3C validator