Theorem iccssxr 13404

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

Syntax hints:   ⊆ wss 3940  (class class class)co 7401  ℝ^*cxr 11244   ≤ cle 11246  [,]cicc 13324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-xr 11249  df-icc 13328

This theorem is referenced by:  eliccxr  13409  supicclub2  13478  lecldbas  23045  ordtresticc  23049  prdsxmetlem  24196  xrge0gsumle  24671  xrge0tsms  24672  metdscn  24694  iccpnfhmeo  24792  xrhmeo  24793  volsup  25407  volsup2  25456  volivth  25458  itg2le  25591  itg2const2  25593  itg2lea  25596  itg2eqa  25597  itg2split  25601  itg2gt0  25612  dvgt0lem1  25857  radcnvlt1  26271  radcnvle  26273  pserulm  26275  psercnlem2  26278  psercnlem1  26279  psercn  26280  pserdvlem1  26281  pserdvlem2  26282  abelthlem3  26287  abelth  26295  logtayl  26510  xrge0infss  32442  xrge0infssd  32443  xrge0subcld  32445  infxrge0lb  32446  infxrge0glb  32447  infxrge0gelb  32448  xrge0base  32651  xrge00  32652  xrge0mulgnn0  32655  xrge0addass  32656  xrge0addgt0  32657  xrge0adddir  32658  xrge0adddi  32659  xrge0npcan  32660  xrge0tsmsd  32677  xrge0slmod  32929  xrge0iifiso  33404  xrge0iifhmeo  33405  xrge0pluscn  33409  xrge0mulc1cn  33410  xrge0tmdALT  33415  lmlimxrge0  33417  pnfneige0  33420  lmxrge0  33421  esummono  33541  esumpad  33542  esumpad2  33543  esumle  33545  gsumesum  33546  esumlub  33547  esumlef  33549  esumcst  33550  esumrnmpt2  33555  esumfsup  33557  esumpinfval  33560  esumpfinvallem  33561  esumpinfsum  33564  esumpmono  33566  esummulc2  33569  esumdivc  33570  hasheuni  33572  esumcvg  33573  esumgect  33577  esum2d  33580  measun  33698  measunl  33703  measiun  33705  voliune  33716  volfiniune  33717  ddemeas  33723  omsfval  33782  omsf  33784  oms0  33785  omssubaddlem  33787  omssubadd  33788  baselcarsg  33794  0elcarsg  33795  difelcarsg  33798  inelcarsg  33799  carsgsigalem  33803  carsggect  33806  carsgclctunlem2  33807  carsgclctunlem3  33808  carsgclctun  33809  omsmeas  33811  pmeasmono  33812  probmeasb  33918  itg2addnclem  37029  ftc1anc  37059  xadd0ge  44515  xrge0nemnfd  44527  xadd0ge2  44536  ge0lere  44730  inficc  44732  iccdificc  44737  fourierdlem1  45309  fourierdlem20  45328  fourierdlem27  45335  fourierdlem87  45394  fge0iccico  45571  gsumge0cl  45572  sge0sn  45580  sge0tsms  45581  sge0xrcl  45586  sge0pr  45595  sge0prle  45602  sge0le  45608  sge0split  45610  sge0p1  45615  sge0rernmpt  45623  sge0xrclmpt  45629  sge0xadd  45636  meaxrcl  45662  meadjun  45663  voliunsge0lem  45673  caragen0  45707  omexrcl  45708  caragenunidm  45709  caragendifcl  45715  omeunle  45717  omeiunle  45718  carageniuncl  45724  ovn0lem  45766  ovnxrcl  45770  hoidmvlelem3  45798  hoidmvlelem4  45799  vonxrcl  45869  icccldii  47739