Theorem iccssxr 12808

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

Syntax hints:   ⊆ wss 3881  (class class class)co 7135  ℝ^*cxr 10663   ≤ cle 10665  [,]cicc 12729

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 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-xr 10668  df-icc 12733

This theorem is referenced by:  eliccxr  12813  supicclub2  12882  lecldbas  21824  ordtresticc  21828  prdsxmetlem  22975  xrge0gsumle  23438  xrge0tsms  23439  metdscn  23461  iccpnfhmeo  23550  xrhmeo  23551  volsup  24160  volsup2  24209  volivth  24211  itg2le  24343  itg2const2  24345  itg2lea  24348  itg2eqa  24349  itg2split  24353  itg2gt0  24364  dvgt0lem1  24605  radcnvlt1  25013  radcnvle  25015  pserulm  25017  psercnlem2  25019  psercnlem1  25020  psercn  25021  pserdvlem1  25022  pserdvlem2  25023  abelthlem3  25028  abelth  25036  logtayl  25251  xrge0infss  30510  xrge0infssd  30511  xrge0subcld  30513  infxrge0lb  30514  infxrge0glb  30515  infxrge0gelb  30516  xrge0base  30719  xrge00  30720  xrge0mulgnn0  30723  xrge0addass  30724  xrge0addgt0  30725  xrge0adddir  30726  xrge0adddi  30727  xrge0npcan  30728  xrge0tsmsd  30742  xrge0slmod  30968  xrge0iifiso  31288  xrge0iifhmeo  31289  xrge0pluscn  31293  xrge0mulc1cn  31294  xrge0tmdALT  31299  lmlimxrge0  31301  pnfneige0  31304  lmxrge0  31305  esummono  31423  esumpad  31424  esumpad2  31425  esumle  31427  gsumesum  31428  esumlub  31429  esumlef  31431  esumcst  31432  esumrnmpt2  31437  esumfsup  31439  esumpinfval  31442  esumpfinvallem  31443  esumpinfsum  31446  esumpmono  31448  esummulc2  31451  esumdivc  31452  hasheuni  31454  esumcvg  31455  esumgect  31459  esum2d  31462  measun  31580  measunl  31585  measiun  31587  voliune  31598  volfiniune  31599  ddemeas  31605  omsfval  31662  omsf  31664  oms0  31665  omssubaddlem  31667  omssubadd  31668  baselcarsg  31674  0elcarsg  31675  difelcarsg  31678  inelcarsg  31679  carsgsigalem  31683  carsggect  31686  carsgclctunlem2  31687  carsgclctunlem3  31688  carsgclctun  31689  omsmeas  31691  pmeasmono  31692  probmeasb  31798  itg2addnclem  35108  ftc1anc  35138  xadd0ge  41952  xrge0nemnfd  41964  xadd0ge2  41973  ge0lere  42169  inficc  42171  iccdificc  42176  fourierdlem1  42750  fourierdlem20  42769  fourierdlem27  42776  fourierdlem87  42835  fge0iccico  43009  gsumge0cl  43010  sge0sn  43018  sge0tsms  43019  sge0xrcl  43024  sge0pr  43033  sge0prle  43040  sge0le  43046  sge0split  43048  sge0p1  43053  sge0rernmpt  43061  sge0xrclmpt  43067  sge0xadd  43074  meaxrcl  43100  meadjun  43101  voliunsge0lem  43111  caragen0  43145  omexrcl  43146  caragenunidm  43147  caragendifcl  43153  omeunle  43155  omeiunle  43156  carageniuncl  43162  ovn0lem  43204  ovnxrcl  43208  hoidmvlelem3  43236  hoidmvlelem4  43237  vonxrcl  43307