Theorem iccssxr 13412

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

Syntax hints:   ⊆ wss 3948  (class class class)co 7412  ℝ^*cxr 11252   ≤ cle 11254  [,]cicc 13332

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7728  ax-cnex 11169  ax-resscn 11170

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7978  df-2nd 7979  df-xr 11257  df-icc 13336

This theorem is referenced by:  eliccxr  13417  supicclub2  13486  lecldbas  22944  ordtresticc  22948  prdsxmetlem  24095  xrge0gsumle  24570  xrge0tsms  24571  metdscn  24593  iccpnfhmeo  24691  xrhmeo  24692  volsup  25306  volsup2  25355  volivth  25357  itg2le  25490  itg2const2  25492  itg2lea  25495  itg2eqa  25496  itg2split  25500  itg2gt0  25511  dvgt0lem1  25755  radcnvlt1  26167  radcnvle  26169  pserulm  26171  psercnlem2  26173  psercnlem1  26174  psercn  26175  pserdvlem1  26176  pserdvlem2  26177  abelthlem3  26182  abelth  26190  logtayl  26405  xrge0infss  32241  xrge0infssd  32242  xrge0subcld  32244  infxrge0lb  32245  infxrge0glb  32246  infxrge0gelb  32247  xrge0base  32454  xrge00  32455  xrge0mulgnn0  32458  xrge0addass  32459  xrge0addgt0  32460  xrge0adddir  32461  xrge0adddi  32462  xrge0npcan  32463  xrge0tsmsd  32480  xrge0slmod  32734  xrge0iifiso  33214  xrge0iifhmeo  33215  xrge0pluscn  33219  xrge0mulc1cn  33220  xrge0tmdALT  33225  lmlimxrge0  33227  pnfneige0  33230  lmxrge0  33231  esummono  33351  esumpad  33352  esumpad2  33353  esumle  33355  gsumesum  33356  esumlub  33357  esumlef  33359  esumcst  33360  esumrnmpt2  33365  esumfsup  33367  esumpinfval  33370  esumpfinvallem  33371  esumpinfsum  33374  esumpmono  33376  esummulc2  33379  esumdivc  33380  hasheuni  33382  esumcvg  33383  esumgect  33387  esum2d  33390  measun  33508  measunl  33513  measiun  33515  voliune  33526  volfiniune  33527  ddemeas  33533  omsfval  33592  omsf  33594  oms0  33595  omssubaddlem  33597  omssubadd  33598  baselcarsg  33604  0elcarsg  33605  difelcarsg  33608  inelcarsg  33609  carsgsigalem  33613  carsggect  33616  carsgclctunlem2  33617  carsgclctunlem3  33618  carsgclctun  33619  omsmeas  33621  pmeasmono  33622  probmeasb  33728  itg2addnclem  36843  ftc1anc  36873  xadd0ge  44329  xrge0nemnfd  44341  xadd0ge2  44350  ge0lere  44544  inficc  44546  iccdificc  44551  fourierdlem1  45123  fourierdlem20  45142  fourierdlem27  45149  fourierdlem87  45208  fge0iccico  45385  gsumge0cl  45386  sge0sn  45394  sge0tsms  45395  sge0xrcl  45400  sge0pr  45409  sge0prle  45416  sge0le  45422  sge0split  45424  sge0p1  45429  sge0rernmpt  45437  sge0xrclmpt  45443  sge0xadd  45450  meaxrcl  45476  meadjun  45477  voliunsge0lem  45487  caragen0  45521  omexrcl  45522  caragenunidm  45523  caragendifcl  45529  omeunle  45531  omeiunle  45532  carageniuncl  45538  ovn0lem  45580  ovnxrcl  45584  hoidmvlelem3  45612  hoidmvlelem4  45613  vonxrcl  45683  icccldii  47639