Theorem iccssxr 13397

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

Syntax hints:   ⊆ wss 3916  (class class class)co 7389  ℝ^*cxr 11213   ≤ cle 11215  [,]cicc 13315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389  ax-un 7713  ax-cnex 11130  ax-resscn 11131

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-fv 6521  df-ov 7392  df-oprab 7393  df-mpo 7394  df-1st 7970  df-2nd 7971  df-xr 11218  df-icc 13319

This theorem is referenced by:  eliccxr  13402  supicclub2  13471  lecldbas  23112  ordtresticc  23116  prdsxmetlem  24262  xrge0gsumle  24728  xrge0tsms  24729  metdscn  24751  iccpnfhmeo  24849  xrhmeo  24850  volsup  25463  volsup2  25512  volivth  25514  itg2le  25646  itg2const2  25648  itg2lea  25651  itg2eqa  25652  itg2split  25656  itg2gt0  25667  dvgt0lem1  25913  radcnvlt1  26333  radcnvle  26335  pserulm  26337  psercnlem2  26340  psercnlem1  26341  psercn  26342  pserdvlem1  26343  pserdvlem2  26344  abelthlem3  26349  abelth  26357  logtayl  26575  xrge0infss  32689  xrge0infssd  32690  xrge0subcld  32692  infxrge0lb  32693  infxrge0glb  32694  infxrge0gelb  32695  xrge0base  32958  xrge00  32959  xrge0mulgnn0  32962  xrge0addass  32963  xrge0addgt0  32964  xrge0adddir  32965  xrge0adddi  32966  xrge0npcan  32967  xrge0tsmsd  33008  xrge0slmod  33325  xrge0iifiso  33931  xrge0iifhmeo  33932  xrge0pluscn  33936  xrge0mulc1cn  33937  xrge0tmdALT  33942  lmlimxrge0  33944  pnfneige0  33947  lmxrge0  33948  esummono  34050  esumpad  34051  esumpad2  34052  esumle  34054  gsumesum  34055  esumlub  34056  esumlef  34058  esumcst  34059  esumrnmpt2  34064  esumfsup  34066  esumpinfval  34069  esumpfinvallem  34070  esumpinfsum  34073  esumpmono  34075  esummulc2  34078  esumdivc  34079  hasheuni  34081  esumcvg  34082  esumgect  34086  esum2d  34089  measun  34207  measunl  34212  measiun  34214  voliune  34225  volfiniune  34226  ddemeas  34232  omsfval  34291  omsf  34293  oms0  34294  omssubaddlem  34296  omssubadd  34297  baselcarsg  34303  0elcarsg  34304  difelcarsg  34307  inelcarsg  34308  carsgsigalem  34312  carsggect  34315  carsgclctunlem2  34316  carsgclctunlem3  34317  carsgclctun  34318  omsmeas  34320  pmeasmono  34321  probmeasb  34427  itg2addnclem  37660  ftc1anc  37690  xadd0ge  45310  xrge0nemnfd  45321  xadd0ge2  45330  ge0lere  45523  inficc  45525  iccdificc  45530  fourierdlem1  46099  fourierdlem20  46118  fourierdlem27  46125  fourierdlem87  46184  fge0iccico  46361  gsumge0cl  46362  sge0sn  46370  sge0tsms  46371  sge0xrcl  46376  sge0pr  46385  sge0prle  46392  sge0le  46398  sge0split  46400  sge0p1  46405  sge0rernmpt  46413  sge0xrclmpt  46419  sge0xadd  46426  meaxrcl  46452  meadjun  46453  voliunsge0lem  46463  caragen0  46497  omexrcl  46498  caragenunidm  46499  caragendifcl  46505  omeunle  46507  omeiunle  46508  carageniuncl  46514  ovn0lem  46556  ovnxrcl  46560  hoidmvlelem3  46588  hoidmvlelem4  46589  vonxrcl  46659  icccldii  48897