Theorem iccssxr 13406

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

Syntax hints:   ⊆ wss 3948  (class class class)co 7408  ℝ^*cxr 11246   ≤ cle 11248  [,]cicc 13326

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-xr 11251  df-icc 13330

This theorem is referenced by:  eliccxr  13411  supicclub2  13480  lecldbas  22722  ordtresticc  22726  prdsxmetlem  23873  xrge0gsumle  24348  xrge0tsms  24349  metdscn  24371  iccpnfhmeo  24460  xrhmeo  24461  volsup  25072  volsup2  25121  volivth  25123  itg2le  25256  itg2const2  25258  itg2lea  25261  itg2eqa  25262  itg2split  25266  itg2gt0  25277  dvgt0lem1  25518  radcnvlt1  25929  radcnvle  25931  pserulm  25933  psercnlem2  25935  psercnlem1  25936  psercn  25937  pserdvlem1  25938  pserdvlem2  25939  abelthlem3  25944  abelth  25952  logtayl  26167  xrge0infss  31968  xrge0infssd  31969  xrge0subcld  31971  infxrge0lb  31972  infxrge0glb  31973  infxrge0gelb  31974  xrge0base  32181  xrge00  32182  xrge0mulgnn0  32185  xrge0addass  32186  xrge0addgt0  32187  xrge0adddir  32188  xrge0adddi  32189  xrge0npcan  32190  xrge0tsmsd  32204  xrge0slmod  32458  xrge0iifiso  32910  xrge0iifhmeo  32911  xrge0pluscn  32915  xrge0mulc1cn  32916  xrge0tmdALT  32921  lmlimxrge0  32923  pnfneige0  32926  lmxrge0  32927  esummono  33047  esumpad  33048  esumpad2  33049  esumle  33051  gsumesum  33052  esumlub  33053  esumlef  33055  esumcst  33056  esumrnmpt2  33061  esumfsup  33063  esumpinfval  33066  esumpfinvallem  33067  esumpinfsum  33070  esumpmono  33072  esummulc2  33075  esumdivc  33076  hasheuni  33078  esumcvg  33079  esumgect  33083  esum2d  33086  measun  33204  measunl  33209  measiun  33211  voliune  33222  volfiniune  33223  ddemeas  33229  omsfval  33288  omsf  33290  oms0  33291  omssubaddlem  33293  omssubadd  33294  baselcarsg  33300  0elcarsg  33301  difelcarsg  33304  inelcarsg  33305  carsgsigalem  33309  carsggect  33312  carsgclctunlem2  33313  carsgclctunlem3  33314  carsgclctun  33315  omsmeas  33317  pmeasmono  33318  probmeasb  33424  itg2addnclem  36534  ftc1anc  36564  xadd0ge  44020  xrge0nemnfd  44032  xadd0ge2  44041  ge0lere  44235  inficc  44237  iccdificc  44242  fourierdlem1  44814  fourierdlem20  44833  fourierdlem27  44840  fourierdlem87  44899  fge0iccico  45076  gsumge0cl  45077  sge0sn  45085  sge0tsms  45086  sge0xrcl  45091  sge0pr  45100  sge0prle  45107  sge0le  45113  sge0split  45115  sge0p1  45120  sge0rernmpt  45128  sge0xrclmpt  45134  sge0xadd  45141  meaxrcl  45167  meadjun  45168  voliunsge0lem  45178  caragen0  45212  omexrcl  45213  caragenunidm  45214  caragendifcl  45220  omeunle  45222  omeiunle  45223  carageniuncl  45229  ovn0lem  45271  ovnxrcl  45275  hoidmvlelem3  45303  hoidmvlelem4  45304  vonxrcl  45374  icccldii  47541