Theorem iccssxr 13347

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

Syntax hints:   ⊆ wss 3890  (class class class)co 7358  ℝ^*cxr 11166   ≤ cle 11168  [,]cicc 13265

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-resscn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-xr 11171  df-icc 13269

This theorem is referenced by:  eliccxr  13352  supicclub2  13421  xrge0base  17529  lecldbas  23162  ordtresticc  23166  prdsxmetlem  24311  xrge0gsumle  24777  xrge0tsms  24778  metdscn  24800  iccpnfhmeo  24890  xrhmeo  24891  volsup  25501  volsup2  25550  volivth  25552  itg2le  25684  itg2const2  25686  itg2lea  25689  itg2eqa  25690  itg2split  25694  itg2gt0  25705  dvgt0lem1  25948  radcnvlt1  26367  radcnvle  26369  pserulm  26371  psercnlem2  26374  psercnlem1  26375  psercn  26376  pserdvlem1  26377  pserdvlem2  26378  abelthlem3  26383  abelth  26391  logtayl  26609  xrge0infss  32823  xrge0infssd  32824  xrge0subcld  32826  infxrge0lb  32827  infxrge0glb  32828  infxrge0gelb  32829  xrge00  33079  xrge0mulgnn0  33080  xrge0addass  33081  xrge0addgt0  33082  xrge0adddir  33083  xrge0adddi  33084  xrge0npcan  33085  xrge0tsmsd  33139  xrge0slmod  33413  xrge0iifiso  34085  xrge0iifhmeo  34086  xrge0pluscn  34090  xrge0mulc1cn  34091  xrge0tmdALT  34096  lmlimxrge0  34098  pnfneige0  34101  lmxrge0  34102  esummono  34204  esumpad  34205  esumpad2  34206  esumle  34208  gsumesum  34209  esumlub  34210  esumlef  34212  esumcst  34213  esumrnmpt2  34218  esumfsup  34220  esumpinfval  34223  esumpfinvallem  34224  esumpinfsum  34227  esumpmono  34229  esummulc2  34232  esumdivc  34233  hasheuni  34235  esumcvg  34236  esumgect  34240  esum2d  34243  measun  34361  measunl  34366  measiun  34368  voliune  34379  volfiniune  34380  ddemeas  34386  omsfval  34444  omsf  34446  oms0  34447  omssubaddlem  34449  omssubadd  34450  baselcarsg  34456  0elcarsg  34457  difelcarsg  34460  inelcarsg  34461  carsgsigalem  34465  carsggect  34468  carsgclctunlem2  34469  carsgclctunlem3  34470  carsgclctun  34471  omsmeas  34473  pmeasmono  34474  probmeasb  34580  itg2addnclem  37983  ftc1anc  38013  xadd0ge  45755  xrge0nemnfd  45765  xadd0ge2  45774  ge0lere  45966  inficc  45968  iccdificc  45973  fourierdlem1  46540  fourierdlem20  46559  fourierdlem27  46566  fourierdlem87  46625  fge0iccico  46802  gsumge0cl  46803  sge0sn  46811  sge0tsms  46812  sge0xrcl  46817  sge0pr  46826  sge0prle  46833  sge0le  46839  sge0split  46841  sge0p1  46846  sge0rernmpt  46854  sge0xrclmpt  46860  sge0xadd  46867  meaxrcl  46893  meadjun  46894  voliunsge0lem  46904  caragen0  46938  omexrcl  46939  caragenunidm  46940  caragendifcl  46946  omeunle  46948  omeiunle  46949  carageniuncl  46955  ovn0lem  46997  ovnxrcl  47001  hoidmvlelem3  47029  hoidmvlelem4  47030  vonxrcl  47100  icccldii  49352