Theorem iccssxr 13351

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

Syntax hints:   ⊆ wss 3905  (class class class)co 7353  ℝ^*cxr 11167   ≤ cle 11169  [,]cicc 13269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-1st 7931  df-2nd 7932  df-xr 11172  df-icc 13273

This theorem is referenced by:  eliccxr  13356  supicclub2  13425  xrge0base  17529  lecldbas  23122  ordtresticc  23126  prdsxmetlem  24272  xrge0gsumle  24738  xrge0tsms  24739  metdscn  24761  iccpnfhmeo  24859  xrhmeo  24860  volsup  25473  volsup2  25522  volivth  25524  itg2le  25656  itg2const2  25658  itg2lea  25661  itg2eqa  25662  itg2split  25666  itg2gt0  25677  dvgt0lem1  25923  radcnvlt1  26343  radcnvle  26345  pserulm  26347  psercnlem2  26350  psercnlem1  26351  psercn  26352  pserdvlem1  26353  pserdvlem2  26354  abelthlem3  26359  abelth  26367  logtayl  26585  xrge0infss  32716  xrge0infssd  32717  xrge0subcld  32719  infxrge0lb  32720  infxrge0glb  32721  infxrge0gelb  32722  xrge00  32981  xrge0mulgnn0  32982  xrge0addass  32983  xrge0addgt0  32984  xrge0adddir  32985  xrge0adddi  32986  xrge0npcan  32987  xrge0tsmsd  33028  xrge0slmod  33295  xrge0iifiso  33901  xrge0iifhmeo  33902  xrge0pluscn  33906  xrge0mulc1cn  33907  xrge0tmdALT  33912  lmlimxrge0  33914  pnfneige0  33917  lmxrge0  33918  esummono  34020  esumpad  34021  esumpad2  34022  esumle  34024  gsumesum  34025  esumlub  34026  esumlef  34028  esumcst  34029  esumrnmpt2  34034  esumfsup  34036  esumpinfval  34039  esumpfinvallem  34040  esumpinfsum  34043  esumpmono  34045  esummulc2  34048  esumdivc  34049  hasheuni  34051  esumcvg  34052  esumgect  34056  esum2d  34059  measun  34177  measunl  34182  measiun  34184  voliune  34195  volfiniune  34196  ddemeas  34202  omsfval  34261  omsf  34263  oms0  34264  omssubaddlem  34266  omssubadd  34267  baselcarsg  34273  0elcarsg  34274  difelcarsg  34277  inelcarsg  34278  carsgsigalem  34282  carsggect  34285  carsgclctunlem2  34286  carsgclctunlem3  34287  carsgclctun  34288  omsmeas  34290  pmeasmono  34291  probmeasb  34397  itg2addnclem  37650  ftc1anc  37680  xadd0ge  45301  xrge0nemnfd  45312  xadd0ge2  45321  ge0lere  45514  inficc  45516  iccdificc  45521  fourierdlem1  46090  fourierdlem20  46109  fourierdlem27  46116  fourierdlem87  46175  fge0iccico  46352  gsumge0cl  46353  sge0sn  46361  sge0tsms  46362  sge0xrcl  46367  sge0pr  46376  sge0prle  46383  sge0le  46389  sge0split  46391  sge0p1  46396  sge0rernmpt  46404  sge0xrclmpt  46410  sge0xadd  46417  meaxrcl  46443  meadjun  46444  voliunsge0lem  46454  caragen0  46488  omexrcl  46489  caragenunidm  46490  caragendifcl  46496  omeunle  46498  omeiunle  46499  carageniuncl  46505  ovn0lem  46547  ovnxrcl  46551  hoidmvlelem3  46579  hoidmvlelem4  46580  vonxrcl  46650  icccldii  48891