Theorem iccssxr 13452

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

Syntax hints:   ⊆ wss 3931  (class class class)co 7413  ℝ^*cxr 11276   ≤ cle 11278  [,]cicc 13372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7996  df-2nd 7997  df-xr 11281  df-icc 13376

This theorem is referenced by:  eliccxr  13457  supicclub2  13526  lecldbas  23173  ordtresticc  23177  prdsxmetlem  24323  xrge0gsumle  24791  xrge0tsms  24792  metdscn  24814  iccpnfhmeo  24912  xrhmeo  24913  volsup  25527  volsup2  25576  volivth  25578  itg2le  25710  itg2const2  25712  itg2lea  25715  itg2eqa  25716  itg2split  25720  itg2gt0  25731  dvgt0lem1  25977  radcnvlt1  26397  radcnvle  26399  pserulm  26401  psercnlem2  26404  psercnlem1  26405  psercn  26406  pserdvlem1  26407  pserdvlem2  26408  abelthlem3  26413  abelth  26421  logtayl  26638  xrge0infss  32701  xrge0infssd  32702  xrge0subcld  32704  infxrge0lb  32705  infxrge0glb  32706  infxrge0gelb  32707  xrge0base  32955  xrge00  32956  xrge0mulgnn0  32959  xrge0addass  32960  xrge0addgt0  32961  xrge0adddir  32962  xrge0adddi  32963  xrge0npcan  32964  xrge0tsmsd  33004  xrge0slmod  33311  xrge0iifiso  33893  xrge0iifhmeo  33894  xrge0pluscn  33898  xrge0mulc1cn  33899  xrge0tmdALT  33904  lmlimxrge0  33906  pnfneige0  33909  lmxrge0  33910  esummono  34014  esumpad  34015  esumpad2  34016  esumle  34018  gsumesum  34019  esumlub  34020  esumlef  34022  esumcst  34023  esumrnmpt2  34028  esumfsup  34030  esumpinfval  34033  esumpfinvallem  34034  esumpinfsum  34037  esumpmono  34039  esummulc2  34042  esumdivc  34043  hasheuni  34045  esumcvg  34046  esumgect  34050  esum2d  34053  measun  34171  measunl  34176  measiun  34178  voliune  34189  volfiniune  34190  ddemeas  34196  omsfval  34255  omsf  34257  oms0  34258  omssubaddlem  34260  omssubadd  34261  baselcarsg  34267  0elcarsg  34268  difelcarsg  34271  inelcarsg  34272  carsgsigalem  34276  carsggect  34279  carsgclctunlem2  34280  carsgclctunlem3  34281  carsgclctun  34282  omsmeas  34284  pmeasmono  34285  probmeasb  34391  itg2addnclem  37637  ftc1anc  37667  xadd0ge  45289  xrge0nemnfd  45300  xadd0ge2  45309  ge0lere  45502  inficc  45504  iccdificc  45509  fourierdlem1  46080  fourierdlem20  46099  fourierdlem27  46106  fourierdlem87  46165  fge0iccico  46342  gsumge0cl  46343  sge0sn  46351  sge0tsms  46352  sge0xrcl  46357  sge0pr  46366  sge0prle  46373  sge0le  46379  sge0split  46381  sge0p1  46386  sge0rernmpt  46394  sge0xrclmpt  46400  sge0xadd  46407  meaxrcl  46433  meadjun  46434  voliunsge0lem  46444  caragen0  46478  omexrcl  46479  caragenunidm  46480  caragendifcl  46486  omeunle  46488  omeiunle  46489  carageniuncl  46495  ovn0lem  46537  ovnxrcl  46541  hoidmvlelem3  46569  hoidmvlelem4  46570  vonxrcl  46640  icccldii  48776