Theorem iccssxr 13375

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

Syntax hints:   ⊆ wss 3883  (class class class)co 7357  ℝ^*cxr 11170   ≤ cle 11172  [,]cicc 13293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pr 5363  ax-un 7679  ax-cnex 11086  ax-resscn 11087

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-iun 4924  df-br 5074  df-opab 5136  df-mpt 5155  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 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7932  df-2nd 7933  df-xr 11175  df-icc 13297

This theorem is referenced by:  eliccxr  13380  supicclub2  13449  xrge0base  17563  lecldbas  23203  ordtresticc  23207  prdsxmetlem  24352  xrge0gsumle  24818  xrge0tsms  24819  metdscn  24841  iccpnfhmeo  24931  xrhmeo  24932  volsup  25542  volsup2  25591  volivth  25593  itg2le  25725  itg2const2  25727  itg2lea  25730  itg2eqa  25731  itg2split  25735  itg2gt0  25746  dvgt0lem1  25988  radcnvlt1  26402  radcnvle  26404  pserulm  26406  psercnlem2  26408  psercnlem1  26409  psercn  26410  pserdvlem1  26411  pserdvlem2  26412  abelthlem3  26417  abelth  26425  logtayl  26643  xrge0infss  32853  xrge0infssd  32854  xrge0subcld  32856  infxrge0lb  32857  infxrge0glb  32858  infxrge0gelb  32859  xrge00  33094  xrge0mulgnn0  33095  xrge0addass  33096  xrge0addgt0  33097  xrge0adddir  33098  xrge0adddi  33099  xrge0npcan  33100  xrge0tsmsd  33155  xrge0slmod  33432  xrge0iifiso  34128  xrge0iifhmeo  34129  xrge0pluscn  34133  xrge0mulc1cn  34134  xrge0tmdALT  34139  lmlimxrge0  34141  pnfneige0  34144  lmxrge0  34145  esummono  34247  esumpad  34248  esumpad2  34249  esumle  34251  gsumesum  34252  esumlub  34253  esumlef  34255  esumcst  34256  esumrnmpt2  34261  esumfsup  34263  esumpinfval  34266  esumpfinvallem  34267  esumpinfsum  34270  esumpmono  34272  esummulc2  34275  esumdivc  34276  hasheuni  34278  esumcvg  34279  esumgect  34283  esum2d  34286  measun  34404  measunl  34409  measiun  34411  voliune  34422  volfiniune  34423  ddemeas  34429  omsfval  34487  omsf  34489  oms0  34490  omssubaddlem  34492  omssubadd  34493  baselcarsg  34499  0elcarsg  34500  difelcarsg  34503  inelcarsg  34504  carsgsigalem  34508  carsggect  34511  carsgclctunlem2  34512  carsgclctunlem3  34513  carsgclctun  34514  omsmeas  34516  pmeasmono  34517  probmeasb  34623  itg2addnclem  38047  ftc1anc  38077  xadd0ge  45775  xrge0nemnfd  45785  xadd0ge2  45794  ge0lere  45985  inficc  45987  iccdificc  45992  fourierdlem1  46559  fourierdlem20  46578  fourierdlem27  46585  fourierdlem87  46644  fge0iccico  46821  gsumge0cl  46822  sge0sn  46830  sge0tsms  46831  sge0xrcl  46836  sge0pr  46845  sge0prle  46852  sge0le  46858  sge0split  46860  sge0p1  46865  sge0rernmpt  46873  sge0xrclmpt  46879  sge0xadd  46886  meaxrcl  46912  meadjun  46913  voliunsge0lem  46923  caragen0  46957  omexrcl  46958  caragenunidm  46959  caragendifcl  46965  omeunle  46967  omeiunle  46968  carageniuncl  46974  ovn0lem  47016  ovnxrcl  47020  hoidmvlelem3  47048  hoidmvlelem4  47049  vonxrcl  47119  icccldii  49417