Theorem iccssxr 13420

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

Syntax hints:   ⊆ wss 3895  (class class class)co 7381  ℝ^*cxr 11201   ≤ cle 11203  [,]cicc 13338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380  ax-un 7703  ax-cnex 11115  ax-resscn 11116

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-fv 6514  df-ov 7384  df-oprab 7385  df-mpo 7386  df-1st 7955  df-2nd 7956  df-xr 11206  df-icc 13342

This theorem is referenced by:  eliccxr  13425  supicclub2  13494  xrge0base  17609  lecldbas  23248  ordtresticc  23252  prdsxmetlem  24397  xrge0gsumle  24863  xrge0tsms  24864  metdscn  24886  iccpnfhmeo  24976  xrhmeo  24977  volsup  25587  volsup2  25636  volivth  25638  itg2le  25770  itg2const2  25772  itg2lea  25775  itg2eqa  25776  itg2split  25780  itg2gt0  25791  dvgt0lem1  26033  radcnvlt1  26447  radcnvle  26449  pserulm  26451  psercnlem2  26453  psercnlem1  26454  psercn  26455  pserdvlem1  26456  pserdvlem2  26457  abelthlem3  26462  abelth  26470  logtayl  26691  xrge0infss  32901  xrge0infssd  32902  xrge0subcld  32904  infxrge0lb  32905  infxrge0glb  32906  infxrge0gelb  32907  xrge00  33142  xrge0mulgnn0  33143  xrge0addass  33144  xrge0addgt0  33145  xrge0adddir  33146  xrge0adddi  33147  xrge0npcan  33148  xrge0tsmsd  33203  xrge0slmod  33480  xrge0iifiso  34176  xrge0iifhmeo  34177  xrge0pluscn  34181  xrge0mulc1cn  34182  xrge0tmdALT  34187  lmlimxrge0  34189  pnfneige0  34192  lmxrge0  34193  esummono  34295  esumpad  34296  esumpad2  34297  esumle  34299  gsumesum  34300  esumlub  34301  esumlef  34303  esumcst  34304  esumrnmpt2  34309  esumfsup  34311  esumpinfval  34314  esumpfinvallem  34315  esumpinfsum  34318  esumpmono  34320  esummulc2  34323  esumdivc  34324  hasheuni  34326  esumcvg  34327  esumgect  34331  esum2d  34334  measun  34452  measunl  34457  measiun  34459  voliune  34470  volfiniune  34471  ddemeas  34477  omsfval  34535  omsf  34537  oms0  34538  omssubaddlem  34540  omssubadd  34541  baselcarsg  34547  0elcarsg  34548  difelcarsg  34551  inelcarsg  34552  carsgsigalem  34556  carsggect  34559  carsgclctunlem2  34560  carsgclctunlem3  34561  carsgclctun  34562  omsmeas  34564  pmeasmono  34565  probmeasb  34671  itg2addnclem  38108  ftc1anc  38138  xadd0ge  45836  xrge0nemnfd  45846  xadd0ge2  45855  ge0lere  46046  inficc  46048  iccdificc  46053  fourierdlem1  46620  fourierdlem20  46639  fourierdlem27  46646  fourierdlem87  46705  fge0iccico  46882  gsumge0cl  46883  sge0sn  46891  sge0tsms  46892  sge0xrcl  46897  sge0pr  46906  sge0prle  46913  sge0le  46919  sge0split  46921  sge0p1  46926  sge0rernmpt  46934  sge0xrclmpt  46940  sge0xadd  46947  meaxrcl  46973  meadjun  46974  voliunsge0lem  46984  caragen0  47018  omexrcl  47019  caragenunidm  47020  caragendifcl  47026  omeunle  47028  omeiunle  47029  carageniuncl  47035  ovn0lem  47077  ovnxrcl  47081  hoidmvlelem3  47109  hoidmvlelem4  47110  vonxrcl  47180  icccldii  49478