Theorem iccssxr 13336

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

Syntax hints:   ⊆ wss 3897  (class class class)co 7352  ℝ^*cxr 11151   ≤ cle 11153  [,]cicc 13254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-cnex 11068  ax-resscn 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-fv 6495  df-ov 7355  df-oprab 7356  df-mpo 7357  df-1st 7927  df-2nd 7928  df-xr 11156  df-icc 13258

This theorem is referenced by:  eliccxr  13341  supicclub2  13410  xrge0base  17517  lecldbas  23140  ordtresticc  23144  prdsxmetlem  24289  xrge0gsumle  24755  xrge0tsms  24756  metdscn  24778  iccpnfhmeo  24876  xrhmeo  24877  volsup  25490  volsup2  25539  volivth  25541  itg2le  25673  itg2const2  25675  itg2lea  25678  itg2eqa  25679  itg2split  25683  itg2gt0  25694  dvgt0lem1  25940  radcnvlt1  26360  radcnvle  26362  pserulm  26364  psercnlem2  26367  psercnlem1  26368  psercn  26369  pserdvlem1  26370  pserdvlem2  26371  abelthlem3  26376  abelth  26384  logtayl  26602  xrge0infss  32750  xrge0infssd  32751  xrge0subcld  32753  infxrge0lb  32754  infxrge0glb  32755  infxrge0gelb  32756  xrge00  33002  xrge0mulgnn0  33003  xrge0addass  33004  xrge0addgt0  33005  xrge0adddir  33006  xrge0adddi  33007  xrge0npcan  33008  xrge0tsmsd  33049  xrge0slmod  33320  xrge0iifiso  33955  xrge0iifhmeo  33956  xrge0pluscn  33960  xrge0mulc1cn  33961  xrge0tmdALT  33966  lmlimxrge0  33968  pnfneige0  33971  lmxrge0  33972  esummono  34074  esumpad  34075  esumpad2  34076  esumle  34078  gsumesum  34079  esumlub  34080  esumlef  34082  esumcst  34083  esumrnmpt2  34088  esumfsup  34090  esumpinfval  34093  esumpfinvallem  34094  esumpinfsum  34097  esumpmono  34099  esummulc2  34102  esumdivc  34103  hasheuni  34105  esumcvg  34106  esumgect  34110  esum2d  34113  measun  34231  measunl  34236  measiun  34238  voliune  34249  volfiniune  34250  ddemeas  34256  omsfval  34314  omsf  34316  oms0  34317  omssubaddlem  34319  omssubadd  34320  baselcarsg  34326  0elcarsg  34327  difelcarsg  34330  inelcarsg  34331  carsgsigalem  34335  carsggect  34338  carsgclctunlem2  34339  carsgclctunlem3  34340  carsgclctun  34341  omsmeas  34343  pmeasmono  34344  probmeasb  34450  itg2addnclem  37717  ftc1anc  37747  xadd0ge  45425  xrge0nemnfd  45436  xadd0ge2  45445  ge0lere  45637  inficc  45639  iccdificc  45644  fourierdlem1  46211  fourierdlem20  46230  fourierdlem27  46237  fourierdlem87  46296  fge0iccico  46473  gsumge0cl  46474  sge0sn  46482  sge0tsms  46483  sge0xrcl  46488  sge0pr  46497  sge0prle  46504  sge0le  46510  sge0split  46512  sge0p1  46517  sge0rernmpt  46525  sge0xrclmpt  46531  sge0xadd  46538  meaxrcl  46564  meadjun  46565  voliunsge0lem  46575  caragen0  46609  omexrcl  46610  caragenunidm  46611  caragendifcl  46617  omeunle  46619  omeiunle  46620  carageniuncl  46626  ovn0lem  46668  ovnxrcl  46672  hoidmvlelem3  46700  hoidmvlelem4  46701  vonxrcl  46771  icccldii  49024