Theorem iccssxr 13447

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

Syntax hints:   ⊆ wss 3926  (class class class)co 7405  ℝ^*cxr 11268   ≤ cle 11270  [,]cicc 13365

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-resscn 11186

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7988  df-2nd 7989  df-xr 11273  df-icc 13369

This theorem is referenced by:  eliccxr  13452  supicclub2  13521  lecldbas  23157  ordtresticc  23161  prdsxmetlem  24307  xrge0gsumle  24773  xrge0tsms  24774  metdscn  24796  iccpnfhmeo  24894  xrhmeo  24895  volsup  25509  volsup2  25558  volivth  25560  itg2le  25692  itg2const2  25694  itg2lea  25697  itg2eqa  25698  itg2split  25702  itg2gt0  25713  dvgt0lem1  25959  radcnvlt1  26379  radcnvle  26381  pserulm  26383  psercnlem2  26386  psercnlem1  26387  psercn  26388  pserdvlem1  26389  pserdvlem2  26390  abelthlem3  26395  abelth  26403  logtayl  26621  xrge0infss  32737  xrge0infssd  32738  xrge0subcld  32740  infxrge0lb  32741  infxrge0glb  32742  infxrge0gelb  32743  xrge0base  33006  xrge00  33007  xrge0mulgnn0  33010  xrge0addass  33011  xrge0addgt0  33012  xrge0adddir  33013  xrge0adddi  33014  xrge0npcan  33015  xrge0tsmsd  33056  xrge0slmod  33363  xrge0iifiso  33966  xrge0iifhmeo  33967  xrge0pluscn  33971  xrge0mulc1cn  33972  xrge0tmdALT  33977  lmlimxrge0  33979  pnfneige0  33982  lmxrge0  33983  esummono  34085  esumpad  34086  esumpad2  34087  esumle  34089  gsumesum  34090  esumlub  34091  esumlef  34093  esumcst  34094  esumrnmpt2  34099  esumfsup  34101  esumpinfval  34104  esumpfinvallem  34105  esumpinfsum  34108  esumpmono  34110  esummulc2  34113  esumdivc  34114  hasheuni  34116  esumcvg  34117  esumgect  34121  esum2d  34124  measun  34242  measunl  34247  measiun  34249  voliune  34260  volfiniune  34261  ddemeas  34267  omsfval  34326  omsf  34328  oms0  34329  omssubaddlem  34331  omssubadd  34332  baselcarsg  34338  0elcarsg  34339  difelcarsg  34342  inelcarsg  34343  carsgsigalem  34347  carsggect  34350  carsgclctunlem2  34351  carsgclctunlem3  34352  carsgclctun  34353  omsmeas  34355  pmeasmono  34356  probmeasb  34462  itg2addnclem  37695  ftc1anc  37725  xadd0ge  45348  xrge0nemnfd  45359  xadd0ge2  45368  ge0lere  45561  inficc  45563  iccdificc  45568  fourierdlem1  46137  fourierdlem20  46156  fourierdlem27  46163  fourierdlem87  46222  fge0iccico  46399  gsumge0cl  46400  sge0sn  46408  sge0tsms  46409  sge0xrcl  46414  sge0pr  46423  sge0prle  46430  sge0le  46436  sge0split  46438  sge0p1  46443  sge0rernmpt  46451  sge0xrclmpt  46457  sge0xadd  46464  meaxrcl  46490  meadjun  46491  voliunsge0lem  46501  caragen0  46535  omexrcl  46536  caragenunidm  46537  caragendifcl  46543  omeunle  46545  omeiunle  46546  carageniuncl  46552  ovn0lem  46594  ovnxrcl  46598  hoidmvlelem3  46626  hoidmvlelem4  46627  vonxrcl  46697  icccldii  48893