Theorem iccssxr 13322

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

Syntax hints:   ⊆ wss 3900  (class class class)co 7341  ℝ^*cxr 11137   ≤ cle 11139  [,]cicc 13240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663  ax-cnex 11054  ax-resscn 11055

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-fv 6485  df-ov 7344  df-oprab 7345  df-mpo 7346  df-1st 7916  df-2nd 7917  df-xr 11142  df-icc 13244

This theorem is referenced by:  eliccxr  13327  supicclub2  13396  xrge0base  17503  lecldbas  23127  ordtresticc  23131  prdsxmetlem  24276  xrge0gsumle  24742  xrge0tsms  24743  metdscn  24765  iccpnfhmeo  24863  xrhmeo  24864  volsup  25477  volsup2  25526  volivth  25528  itg2le  25660  itg2const2  25662  itg2lea  25665  itg2eqa  25666  itg2split  25670  itg2gt0  25681  dvgt0lem1  25927  radcnvlt1  26347  radcnvle  26349  pserulm  26351  psercnlem2  26354  psercnlem1  26355  psercn  26356  pserdvlem1  26357  pserdvlem2  26358  abelthlem3  26363  abelth  26371  logtayl  26589  xrge0infss  32733  xrge0infssd  32734  xrge0subcld  32736  infxrge0lb  32737  infxrge0glb  32738  infxrge0gelb  32739  xrge00  32985  xrge0mulgnn0  32986  xrge0addass  32987  xrge0addgt0  32988  xrge0adddir  32989  xrge0adddi  32990  xrge0npcan  32991  xrge0tsmsd  33032  xrge0slmod  33303  xrge0iifiso  33938  xrge0iifhmeo  33939  xrge0pluscn  33943  xrge0mulc1cn  33944  xrge0tmdALT  33949  lmlimxrge0  33951  pnfneige0  33954  lmxrge0  33955  esummono  34057  esumpad  34058  esumpad2  34059  esumle  34061  gsumesum  34062  esumlub  34063  esumlef  34065  esumcst  34066  esumrnmpt2  34071  esumfsup  34073  esumpinfval  34076  esumpfinvallem  34077  esumpinfsum  34080  esumpmono  34082  esummulc2  34085  esumdivc  34086  hasheuni  34088  esumcvg  34089  esumgect  34093  esum2d  34096  measun  34214  measunl  34219  measiun  34221  voliune  34232  volfiniune  34233  ddemeas  34239  omsfval  34297  omsf  34299  oms0  34300  omssubaddlem  34302  omssubadd  34303  baselcarsg  34309  0elcarsg  34310  difelcarsg  34313  inelcarsg  34314  carsgsigalem  34318  carsggect  34321  carsgclctunlem2  34322  carsgclctunlem3  34323  carsgclctun  34324  omsmeas  34326  pmeasmono  34327  probmeasb  34433  itg2addnclem  37690  ftc1anc  37720  xadd0ge  45339  xrge0nemnfd  45350  xadd0ge2  45359  ge0lere  45551  inficc  45553  iccdificc  45558  fourierdlem1  46125  fourierdlem20  46144  fourierdlem27  46151  fourierdlem87  46210  fge0iccico  46387  gsumge0cl  46388  sge0sn  46396  sge0tsms  46397  sge0xrcl  46402  sge0pr  46411  sge0prle  46418  sge0le  46424  sge0split  46426  sge0p1  46431  sge0rernmpt  46439  sge0xrclmpt  46445  sge0xadd  46452  meaxrcl  46478  meadjun  46479  voliunsge0lem  46489  caragen0  46523  omexrcl  46524  caragenunidm  46525  caragendifcl  46531  omeunle  46533  omeiunle  46534  carageniuncl  46540  ovn0lem  46582  ovnxrcl  46586  hoidmvlelem3  46614  hoidmvlelem4  46615  vonxrcl  46685  icccldii  48929