Theorem iccssxr 13490

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

Syntax hints:   ⊆ wss 3976  (class class class)co 7448  ℝ^*cxr 11323   ≤ cle 11325  [,]cicc 13410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-xr 11328  df-icc 13414

This theorem is referenced by:  eliccxr  13495  supicclub2  13564  lecldbas  23248  ordtresticc  23252  prdsxmetlem  24399  xrge0gsumle  24874  xrge0tsms  24875  metdscn  24897  iccpnfhmeo  24995  xrhmeo  24996  volsup  25610  volsup2  25659  volivth  25661  itg2le  25794  itg2const2  25796  itg2lea  25799  itg2eqa  25800  itg2split  25804  itg2gt0  25815  dvgt0lem1  26061  radcnvlt1  26479  radcnvle  26481  pserulm  26483  psercnlem2  26486  psercnlem1  26487  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  abelthlem3  26495  abelth  26503  logtayl  26720  xrge0infss  32767  xrge0infssd  32768  xrge0subcld  32770  infxrge0lb  32771  infxrge0glb  32772  infxrge0gelb  32773  xrge0base  32997  xrge00  32998  xrge0mulgnn0  33001  xrge0addass  33002  xrge0addgt0  33003  xrge0adddir  33004  xrge0adddi  33005  xrge0npcan  33006  xrge0tsmsd  33041  xrge0slmod  33341  xrge0iifiso  33881  xrge0iifhmeo  33882  xrge0pluscn  33886  xrge0mulc1cn  33887  xrge0tmdALT  33892  lmlimxrge0  33894  pnfneige0  33897  lmxrge0  33898  esummono  34018  esumpad  34019  esumpad2  34020  esumle  34022  gsumesum  34023  esumlub  34024  esumlef  34026  esumcst  34027  esumrnmpt2  34032  esumfsup  34034  esumpinfval  34037  esumpfinvallem  34038  esumpinfsum  34041  esumpmono  34043  esummulc2  34046  esumdivc  34047  hasheuni  34049  esumcvg  34050  esumgect  34054  esum2d  34057  measun  34175  measunl  34180  measiun  34182  voliune  34193  volfiniune  34194  ddemeas  34200  omsfval  34259  omsf  34261  oms0  34262  omssubaddlem  34264  omssubadd  34265  baselcarsg  34271  0elcarsg  34272  difelcarsg  34275  inelcarsg  34276  carsgsigalem  34280  carsggect  34283  carsgclctunlem2  34284  carsgclctunlem3  34285  carsgclctun  34286  omsmeas  34288  pmeasmono  34289  probmeasb  34395  itg2addnclem  37631  ftc1anc  37661  xadd0ge  45235  xrge0nemnfd  45247  xadd0ge2  45256  ge0lere  45450  inficc  45452  iccdificc  45457  fourierdlem1  46029  fourierdlem20  46048  fourierdlem27  46055  fourierdlem87  46114  fge0iccico  46291  gsumge0cl  46292  sge0sn  46300  sge0tsms  46301  sge0xrcl  46306  sge0pr  46315  sge0prle  46322  sge0le  46328  sge0split  46330  sge0p1  46335  sge0rernmpt  46343  sge0xrclmpt  46349  sge0xadd  46356  meaxrcl  46382  meadjun  46383  voliunsge0lem  46393  caragen0  46427  omexrcl  46428  caragenunidm  46429  caragendifcl  46435  omeunle  46437  omeiunle  46438  carageniuncl  46444  ovn0lem  46486  ovnxrcl  46490  hoidmvlelem3  46518  hoidmvlelem4  46519  vonxrcl  46589  icccldii  48598