Theorem iccssxr 13350

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.

Step	Hyp	Ref	Expression
1		df-icc 13272	. 2 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
2	1	ixxssxr 13277	1 ⊢ (𝐴[,]𝐵) ⊆ ℝ*

Syntax hints:   ⊆ wss 3902  (class class class)co 7360  ℝ^*cxr 11169   ≤ cle 11171  [,]cicc 13268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-xr 11174  df-icc 13272

This theorem is referenced by:  eliccxr  13355  supicclub2  13424  xrge0base  17532  lecldbas  23167  ordtresticc  23171  prdsxmetlem  24316  xrge0gsumle  24782  xrge0tsms  24783  metdscn  24805  iccpnfhmeo  24903  xrhmeo  24904  volsup  25517  volsup2  25566  volivth  25568  itg2le  25700  itg2const2  25702  itg2lea  25705  itg2eqa  25706  itg2split  25710  itg2gt0  25721  dvgt0lem1  25967  radcnvlt1  26387  radcnvle  26389  pserulm  26391  psercnlem2  26394  psercnlem1  26395  psercn  26396  pserdvlem1  26397  pserdvlem2  26398  abelthlem3  26403  abelth  26411  logtayl  26629  xrge0infss  32821  xrge0infssd  32822  xrge0subcld  32824  infxrge0lb  32825  infxrge0glb  32826  infxrge0gelb  32827  xrge00  33077  xrge0mulgnn0  33078  xrge0addass  33079  xrge0addgt0  33080  xrge0adddir  33081  xrge0adddi  33082  xrge0npcan  33083  xrge0tsmsd  33136  xrge0slmod  33410  xrge0iifiso  34073  xrge0iifhmeo  34074  xrge0pluscn  34078  xrge0mulc1cn  34079  xrge0tmdALT  34084  lmlimxrge0  34086  pnfneige0  34089  lmxrge0  34090  esummono  34192  esumpad  34193  esumpad2  34194  esumle  34196  gsumesum  34197  esumlub  34198  esumlef  34200  esumcst  34201  esumrnmpt2  34206  esumfsup  34208  esumpinfval  34211  esumpfinvallem  34212  esumpinfsum  34215  esumpmono  34217  esummulc2  34220  esumdivc  34221  hasheuni  34223  esumcvg  34224  esumgect  34228  esum2d  34231  measun  34349  measunl  34354  measiun  34356  voliune  34367  volfiniune  34368  ddemeas  34374  omsfval  34432  omsf  34434  oms0  34435  omssubaddlem  34437  omssubadd  34438  baselcarsg  34444  0elcarsg  34445  difelcarsg  34448  inelcarsg  34449  carsgsigalem  34453  carsggect  34456  carsgclctunlem2  34457  carsgclctunlem3  34458  carsgclctun  34459  omsmeas  34461  pmeasmono  34462  probmeasb  34568  itg2addnclem  37843  ftc1anc  37873  xadd0ge  45603  xrge0nemnfd  45613  xadd0ge2  45622  ge0lere  45814  inficc  45816  iccdificc  45821  fourierdlem1  46388  fourierdlem20  46407  fourierdlem27  46414  fourierdlem87  46473  fge0iccico  46650  gsumge0cl  46651  sge0sn  46659  sge0tsms  46660  sge0xrcl  46665  sge0pr  46674  sge0prle  46681  sge0le  46687  sge0split  46689  sge0p1  46694  sge0rernmpt  46702  sge0xrclmpt  46708  sge0xadd  46715  meaxrcl  46741  meadjun  46742  voliunsge0lem  46752  caragen0  46786  omexrcl  46787  caragenunidm  46788  caragendifcl  46794  omeunle  46796  omeiunle  46797  carageniuncl  46803  ovn0lem  46845  ovnxrcl  46849  hoidmvlelem3  46877  hoidmvlelem4  46878  vonxrcl  46948  icccldii  49200