Theorem iccssxr 13467

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

Syntax hints:   ⊆ wss 3963  (class class class)co 7431  ℝ^*cxr 11292   ≤ cle 11294  [,]cicc 13387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-xr 11297  df-icc 13391

This theorem is referenced by:  eliccxr  13472  supicclub2  13541  lecldbas  23243  ordtresticc  23247  prdsxmetlem  24394  xrge0gsumle  24869  xrge0tsms  24870  metdscn  24892  iccpnfhmeo  24990  xrhmeo  24991  volsup  25605  volsup2  25654  volivth  25656  itg2le  25789  itg2const2  25791  itg2lea  25794  itg2eqa  25795  itg2split  25799  itg2gt0  25810  dvgt0lem1  26056  radcnvlt1  26476  radcnvle  26478  pserulm  26480  psercnlem2  26483  psercnlem1  26484  psercn  26485  pserdvlem1  26486  pserdvlem2  26487  abelthlem3  26492  abelth  26500  logtayl  26717  xrge0infss  32771  xrge0infssd  32772  xrge0subcld  32774  infxrge0lb  32775  infxrge0glb  32776  infxrge0gelb  32777  xrge0base  32999  xrge00  33000  xrge0mulgnn0  33003  xrge0addass  33004  xrge0addgt0  33005  xrge0adddir  33006  xrge0adddi  33007  xrge0npcan  33008  xrge0tsmsd  33048  xrge0slmod  33356  xrge0iifiso  33896  xrge0iifhmeo  33897  xrge0pluscn  33901  xrge0mulc1cn  33902  xrge0tmdALT  33907  lmlimxrge0  33909  pnfneige0  33912  lmxrge0  33913  esummono  34035  esumpad  34036  esumpad2  34037  esumle  34039  gsumesum  34040  esumlub  34041  esumlef  34043  esumcst  34044  esumrnmpt2  34049  esumfsup  34051  esumpinfval  34054  esumpfinvallem  34055  esumpinfsum  34058  esumpmono  34060  esummulc2  34063  esumdivc  34064  hasheuni  34066  esumcvg  34067  esumgect  34071  esum2d  34074  measun  34192  measunl  34197  measiun  34199  voliune  34210  volfiniune  34211  ddemeas  34217  omsfval  34276  omsf  34278  oms0  34279  omssubaddlem  34281  omssubadd  34282  baselcarsg  34288  0elcarsg  34289  difelcarsg  34292  inelcarsg  34293  carsgsigalem  34297  carsggect  34300  carsgclctunlem2  34301  carsgclctunlem3  34302  carsgclctun  34303  omsmeas  34305  pmeasmono  34306  probmeasb  34412  itg2addnclem  37658  ftc1anc  37688  xadd0ge  45271  xrge0nemnfd  45282  xadd0ge2  45291  ge0lere  45485  inficc  45487  iccdificc  45492  fourierdlem1  46064  fourierdlem20  46083  fourierdlem27  46090  fourierdlem87  46149  fge0iccico  46326  gsumge0cl  46327  sge0sn  46335  sge0tsms  46336  sge0xrcl  46341  sge0pr  46350  sge0prle  46357  sge0le  46363  sge0split  46365  sge0p1  46370  sge0rernmpt  46378  sge0xrclmpt  46384  sge0xadd  46391  meaxrcl  46417  meadjun  46418  voliunsge0lem  46428  caragen0  46462  omexrcl  46463  caragenunidm  46464  caragendifcl  46470  omeunle  46472  omeiunle  46473  carageniuncl  46479  ovn0lem  46521  ovnxrcl  46525  hoidmvlelem3  46553  hoidmvlelem4  46554  vonxrcl  46624  icccldii  48715