Theorem iccssxr 13383

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

Syntax hints:   ⊆ wss 3890  (class class class)co 7367  ℝ^*cxr 11178   ≤ cle 11180  [,]cicc 13301

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 5232  ax-nul 5242  ax-pr 5376  ax-un 7689  ax-cnex 11094  ax-resscn 11095

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 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-xr 11183  df-icc 13305

This theorem is referenced by:  eliccxr  13388  supicclub2  13457  xrge0base  17571  lecldbas  23184  ordtresticc  23188  prdsxmetlem  24333  xrge0gsumle  24799  xrge0tsms  24800  metdscn  24822  iccpnfhmeo  24912  xrhmeo  24913  volsup  25523  volsup2  25572  volivth  25574  itg2le  25706  itg2const2  25708  itg2lea  25711  itg2eqa  25712  itg2split  25716  itg2gt0  25727  dvgt0lem1  25969  radcnvlt1  26383  radcnvle  26385  pserulm  26387  psercnlem2  26389  psercnlem1  26390  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  abelthlem3  26398  abelth  26406  logtayl  26624  xrge0infss  32833  xrge0infssd  32834  xrge0subcld  32836  infxrge0lb  32837  infxrge0glb  32838  infxrge0gelb  32839  xrge00  33074  xrge0mulgnn0  33075  xrge0addass  33076  xrge0addgt0  33077  xrge0adddir  33078  xrge0adddi  33079  xrge0npcan  33080  xrge0tsmsd  33134  xrge0slmod  33408  xrge0iifiso  34079  xrge0iifhmeo  34080  xrge0pluscn  34084  xrge0mulc1cn  34085  xrge0tmdALT  34090  lmlimxrge0  34092  pnfneige0  34095  lmxrge0  34096  esummono  34198  esumpad  34199  esumpad2  34200  esumle  34202  gsumesum  34203  esumlub  34204  esumlef  34206  esumcst  34207  esumrnmpt2  34212  esumfsup  34214  esumpinfval  34217  esumpfinvallem  34218  esumpinfsum  34221  esumpmono  34223  esummulc2  34226  esumdivc  34227  hasheuni  34229  esumcvg  34230  esumgect  34234  esum2d  34237  measun  34355  measunl  34360  measiun  34362  voliune  34373  volfiniune  34374  ddemeas  34380  omsfval  34438  omsf  34440  oms0  34441  omssubaddlem  34443  omssubadd  34444  baselcarsg  34450  0elcarsg  34451  difelcarsg  34454  inelcarsg  34455  carsgsigalem  34459  carsggect  34462  carsgclctunlem2  34463  carsgclctunlem3  34464  carsgclctun  34465  omsmeas  34467  pmeasmono  34468  probmeasb  34574  itg2addnclem  37992  ftc1anc  38022  xadd0ge  45752  xrge0nemnfd  45762  xadd0ge2  45771  ge0lere  45962  inficc  45964  iccdificc  45969  fourierdlem1  46536  fourierdlem20  46555  fourierdlem27  46562  fourierdlem87  46621  fge0iccico  46798  gsumge0cl  46799  sge0sn  46807  sge0tsms  46808  sge0xrcl  46813  sge0pr  46822  sge0prle  46829  sge0le  46835  sge0split  46837  sge0p1  46842  sge0rernmpt  46850  sge0xrclmpt  46856  sge0xadd  46863  meaxrcl  46889  meadjun  46890  voliunsge0lem  46900  caragen0  46934  omexrcl  46935  caragenunidm  46936  caragendifcl  46942  omeunle  46944  omeiunle  46945  carageniuncl  46951  ovn0lem  46993  ovnxrcl  46997  hoidmvlelem3  47025  hoidmvlelem4  47026  vonxrcl  47096  icccldii  49388