Theorem iccssxr 13372

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

Syntax hints:   ⊆ wss 3885  (class class class)co 7356  ℝ^*cxr 11167   ≤ cle 11169  [,]cicc 13290

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 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7678  ax-cnex 11083  ax-resscn 11084

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-fv 6495  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-xr 11172  df-icc 13294

This theorem is referenced by:  eliccxr  13377  supicclub2  13446  xrge0base  17560  lecldbas  23172  ordtresticc  23176  prdsxmetlem  24321  xrge0gsumle  24787  xrge0tsms  24788  metdscn  24810  iccpnfhmeo  24900  xrhmeo  24901  volsup  25511  volsup2  25560  volivth  25562  itg2le  25694  itg2const2  25696  itg2lea  25699  itg2eqa  25700  itg2split  25704  itg2gt0  25715  dvgt0lem1  25957  radcnvlt1  26371  radcnvle  26373  pserulm  26375  psercnlem2  26377  psercnlem1  26378  psercn  26379  pserdvlem1  26380  pserdvlem2  26381  abelthlem3  26386  abelth  26394  logtayl  26612  xrge0infss  32821  xrge0infssd  32822  xrge0subcld  32824  infxrge0lb  32825  infxrge0glb  32826  infxrge0gelb  32827  xrge00  33062  xrge0mulgnn0  33063  xrge0addass  33064  xrge0addgt0  33065  xrge0adddir  33066  xrge0adddi  33067  xrge0npcan  33068  xrge0tsmsd  33122  xrge0slmod  33396  xrge0iifiso  34067  xrge0iifhmeo  34068  xrge0pluscn  34072  xrge0mulc1cn  34073  xrge0tmdALT  34078  lmlimxrge0  34080  pnfneige0  34083  lmxrge0  34084  esummono  34186  esumpad  34187  esumpad2  34188  esumle  34190  gsumesum  34191  esumlub  34192  esumlef  34194  esumcst  34195  esumrnmpt2  34200  esumfsup  34202  esumpinfval  34205  esumpfinvallem  34206  esumpinfsum  34209  esumpmono  34211  esummulc2  34214  esumdivc  34215  hasheuni  34217  esumcvg  34218  esumgect  34222  esum2d  34225  measun  34343  measunl  34348  measiun  34350  voliune  34361  volfiniune  34362  ddemeas  34368  omsfval  34426  omsf  34428  oms0  34429  omssubaddlem  34431  omssubadd  34432  baselcarsg  34438  0elcarsg  34439  difelcarsg  34442  inelcarsg  34443  carsgsigalem  34447  carsggect  34450  carsgclctunlem2  34451  carsgclctunlem3  34452  carsgclctun  34453  omsmeas  34455  pmeasmono  34456  probmeasb  34562  itg2addnclem  37980  ftc1anc  38010  xadd0ge  45740  xrge0nemnfd  45750  xadd0ge2  45759  ge0lere  45950  inficc  45952  iccdificc  45957  fourierdlem1  46524  fourierdlem20  46543  fourierdlem27  46550  fourierdlem87  46609  fge0iccico  46786  gsumge0cl  46787  sge0sn  46795  sge0tsms  46796  sge0xrcl  46801  sge0pr  46810  sge0prle  46817  sge0le  46823  sge0split  46825  sge0p1  46830  sge0rernmpt  46838  sge0xrclmpt  46844  sge0xadd  46851  meaxrcl  46877  meadjun  46878  voliunsge0lem  46888  caragen0  46922  omexrcl  46923  caragenunidm  46924  caragendifcl  46930  omeunle  46932  omeiunle  46933  carageniuncl  46939  ovn0lem  46981  ovnxrcl  46985  hoidmvlelem3  47013  hoidmvlelem4  47014  vonxrcl  47084  icccldii  49382