Theorem iccssxr 13351

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 13273	. 2 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
2	1	ixxssxr 13278	1 ⊢ (𝐴[,]𝐵) ⊆ ℝ*

Syntax hints:   ⊆ wss 3902  (class class class)co 7361  ℝ^*cxr 11170   ≤ cle 11172  [,]cicc 13269

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 7683  ax-cnex 11087  ax-resscn 11088

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 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-xr 11175  df-icc 13273

This theorem is referenced by:  eliccxr  13356  supicclub2  13425  xrge0base  17533  lecldbas  23168  ordtresticc  23172  prdsxmetlem  24317  xrge0gsumle  24783  xrge0tsms  24784  metdscn  24806  iccpnfhmeo  24904  xrhmeo  24905  volsup  25518  volsup2  25567  volivth  25569  itg2le  25701  itg2const2  25703  itg2lea  25706  itg2eqa  25707  itg2split  25711  itg2gt0  25722  dvgt0lem1  25968  radcnvlt1  26388  radcnvle  26390  pserulm  26392  psercnlem2  26395  psercnlem1  26396  psercn  26397  pserdvlem1  26398  pserdvlem2  26399  abelthlem3  26404  abelth  26412  logtayl  26630  xrge0infss  32843  xrge0infssd  32844  xrge0subcld  32846  infxrge0lb  32847  infxrge0glb  32848  infxrge0gelb  32849  xrge00  33099  xrge0mulgnn0  33100  xrge0addass  33101  xrge0addgt0  33102  xrge0adddir  33103  xrge0adddi  33104  xrge0npcan  33105  xrge0tsmsd  33159  xrge0slmod  33433  xrge0iifiso  34105  xrge0iifhmeo  34106  xrge0pluscn  34110  xrge0mulc1cn  34111  xrge0tmdALT  34116  lmlimxrge0  34118  pnfneige0  34121  lmxrge0  34122  esummono  34224  esumpad  34225  esumpad2  34226  esumle  34228  gsumesum  34229  esumlub  34230  esumlef  34232  esumcst  34233  esumrnmpt2  34238  esumfsup  34240  esumpinfval  34243  esumpfinvallem  34244  esumpinfsum  34247  esumpmono  34249  esummulc2  34252  esumdivc  34253  hasheuni  34255  esumcvg  34256  esumgect  34260  esum2d  34263  measun  34381  measunl  34386  measiun  34388  voliune  34399  volfiniune  34400  ddemeas  34406  omsfval  34464  omsf  34466  oms0  34467  omssubaddlem  34469  omssubadd  34470  baselcarsg  34476  0elcarsg  34477  difelcarsg  34480  inelcarsg  34481  carsgsigalem  34485  carsggect  34488  carsgclctunlem2  34489  carsgclctunlem3  34490  carsgclctun  34491  omsmeas  34493  pmeasmono  34494  probmeasb  34600  itg2addnclem  37885  ftc1anc  37915  xadd0ge  45644  xrge0nemnfd  45654  xadd0ge2  45663  ge0lere  45855  inficc  45857  iccdificc  45862  fourierdlem1  46429  fourierdlem20  46448  fourierdlem27  46455  fourierdlem87  46514  fge0iccico  46691  gsumge0cl  46692  sge0sn  46700  sge0tsms  46701  sge0xrcl  46706  sge0pr  46715  sge0prle  46722  sge0le  46728  sge0split  46730  sge0p1  46735  sge0rernmpt  46743  sge0xrclmpt  46749  sge0xadd  46756  meaxrcl  46782  meadjun  46783  voliunsge0lem  46793  caragen0  46827  omexrcl  46828  caragenunidm  46829  caragendifcl  46835  omeunle  46837  omeiunle  46838  carageniuncl  46844  ovn0lem  46886  ovnxrcl  46890  hoidmvlelem3  46918  hoidmvlelem4  46919  vonxrcl  46989  icccldii  49241