Theorem iccssxr 13431

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

Syntax hints:   ⊆ wss 3944  (class class class)co 7414  ℝ^*cxr 11269   ≤ cle 11271  [,]cicc 13351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-xr 11274  df-icc 13355

This theorem is referenced by:  eliccxr  13436  supicclub2  13505  lecldbas  23110  ordtresticc  23114  prdsxmetlem  24261  xrge0gsumle  24736  xrge0tsms  24737  metdscn  24759  iccpnfhmeo  24857  xrhmeo  24858  volsup  25472  volsup2  25521  volivth  25523  itg2le  25656  itg2const2  25658  itg2lea  25661  itg2eqa  25662  itg2split  25666  itg2gt0  25677  dvgt0lem1  25922  radcnvlt1  26341  radcnvle  26343  pserulm  26345  psercnlem2  26348  psercnlem1  26349  psercn  26350  pserdvlem1  26351  pserdvlem2  26352  abelthlem3  26357  abelth  26365  logtayl  26581  xrge0infss  32514  xrge0infssd  32515  xrge0subcld  32517  infxrge0lb  32518  infxrge0glb  32519  infxrge0gelb  32520  xrge0base  32723  xrge00  32724  xrge0mulgnn0  32727  xrge0addass  32728  xrge0addgt0  32729  xrge0adddir  32730  xrge0adddi  32731  xrge0npcan  32732  xrge0tsmsd  32749  xrge0slmod  33000  xrge0iifiso  33472  xrge0iifhmeo  33473  xrge0pluscn  33477  xrge0mulc1cn  33478  xrge0tmdALT  33483  lmlimxrge0  33485  pnfneige0  33488  lmxrge0  33489  esummono  33609  esumpad  33610  esumpad2  33611  esumle  33613  gsumesum  33614  esumlub  33615  esumlef  33617  esumcst  33618  esumrnmpt2  33623  esumfsup  33625  esumpinfval  33628  esumpfinvallem  33629  esumpinfsum  33632  esumpmono  33634  esummulc2  33637  esumdivc  33638  hasheuni  33640  esumcvg  33641  esumgect  33645  esum2d  33648  measun  33766  measunl  33771  measiun  33773  voliune  33784  volfiniune  33785  ddemeas  33791  omsfval  33850  omsf  33852  oms0  33853  omssubaddlem  33855  omssubadd  33856  baselcarsg  33862  0elcarsg  33863  difelcarsg  33866  inelcarsg  33867  carsgsigalem  33871  carsggect  33874  carsgclctunlem2  33875  carsgclctunlem3  33876  carsgclctun  33877  omsmeas  33879  pmeasmono  33880  probmeasb  33986  itg2addnclem  37079  ftc1anc  37109  xadd0ge  44625  xrge0nemnfd  44637  xadd0ge2  44646  ge0lere  44840  inficc  44842  iccdificc  44847  fourierdlem1  45419  fourierdlem20  45438  fourierdlem27  45445  fourierdlem87  45504  fge0iccico  45681  gsumge0cl  45682  sge0sn  45690  sge0tsms  45691  sge0xrcl  45696  sge0pr  45705  sge0prle  45712  sge0le  45718  sge0split  45720  sge0p1  45725  sge0rernmpt  45733  sge0xrclmpt  45739  sge0xadd  45746  meaxrcl  45772  meadjun  45773  voliunsge0lem  45783  caragen0  45817  omexrcl  45818  caragenunidm  45819  caragendifcl  45825  omeunle  45827  omeiunle  45828  carageniuncl  45834  ovn0lem  45876  ovnxrcl  45880  hoidmvlelem3  45908  hoidmvlelem4  45909  vonxrcl  45979  icccldii  47860