Theorem iccssxr 12862

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

Syntax hints:   ⊆ wss 3858  (class class class)co 7150  ℝ^*cxr 10712   ≤ cle 10714  [,]cicc 12782

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7693  df-2nd 7694  df-xr 10717  df-icc 12786

This theorem is referenced by:  eliccxr  12867  supicclub2  12936  lecldbas  21919  ordtresticc  21923  prdsxmetlem  23070  xrge0gsumle  23534  xrge0tsms  23535  metdscn  23557  iccpnfhmeo  23646  xrhmeo  23647  volsup  24256  volsup2  24305  volivth  24307  itg2le  24439  itg2const2  24441  itg2lea  24444  itg2eqa  24445  itg2split  24449  itg2gt0  24460  dvgt0lem1  24701  radcnvlt1  25112  radcnvle  25114  pserulm  25116  psercnlem2  25118  psercnlem1  25119  psercn  25120  pserdvlem1  25121  pserdvlem2  25122  abelthlem3  25127  abelth  25135  logtayl  25350  xrge0infss  30607  xrge0infssd  30608  xrge0subcld  30610  infxrge0lb  30611  infxrge0glb  30612  infxrge0gelb  30613  xrge0base  30820  xrge00  30821  xrge0mulgnn0  30824  xrge0addass  30825  xrge0addgt0  30826  xrge0adddir  30827  xrge0adddi  30828  xrge0npcan  30829  xrge0tsmsd  30843  xrge0slmod  31069  xrge0iifiso  31406  xrge0iifhmeo  31407  xrge0pluscn  31411  xrge0mulc1cn  31412  xrge0tmdALT  31417  lmlimxrge0  31419  pnfneige0  31422  lmxrge0  31423  esummono  31541  esumpad  31542  esumpad2  31543  esumle  31545  gsumesum  31546  esumlub  31547  esumlef  31549  esumcst  31550  esumrnmpt2  31555  esumfsup  31557  esumpinfval  31560  esumpfinvallem  31561  esumpinfsum  31564  esumpmono  31566  esummulc2  31569  esumdivc  31570  hasheuni  31572  esumcvg  31573  esumgect  31577  esum2d  31580  measun  31698  measunl  31703  measiun  31705  voliune  31716  volfiniune  31717  ddemeas  31723  omsfval  31780  omsf  31782  oms0  31783  omssubaddlem  31785  omssubadd  31786  baselcarsg  31792  0elcarsg  31793  difelcarsg  31796  inelcarsg  31797  carsgsigalem  31801  carsggect  31804  carsgclctunlem2  31805  carsgclctunlem3  31806  carsgclctun  31807  omsmeas  31809  pmeasmono  31810  probmeasb  31916  itg2addnclem  35388  ftc1anc  35418  xadd0ge  42320  xrge0nemnfd  42332  xadd0ge2  42341  ge0lere  42535  inficc  42537  iccdificc  42542  fourierdlem1  43116  fourierdlem20  43135  fourierdlem27  43142  fourierdlem87  43201  fge0iccico  43375  gsumge0cl  43376  sge0sn  43384  sge0tsms  43385  sge0xrcl  43390  sge0pr  43399  sge0prle  43406  sge0le  43412  sge0split  43414  sge0p1  43419  sge0rernmpt  43427  sge0xrclmpt  43433  sge0xadd  43440  meaxrcl  43466  meadjun  43467  voliunsge0lem  43477  caragen0  43511  omexrcl  43512  caragenunidm  43513  caragendifcl  43519  omeunle  43521  omeiunle  43522  carageniuncl  43528  ovn0lem  43570  ovnxrcl  43574  hoidmvlelem3  43602  hoidmvlelem4  43603  vonxrcl  43673