Theorem iccssxr 12813

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

Syntax hints:   ⊆ wss 3935  (class class class)co 7150  ℝ^*cxr 10668   ≤ cle 10670  [,]cicc 12735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-xr 10673  df-icc 12739

This theorem is referenced by:  eliccxr  12817  supicclub2  12883  lecldbas  21821  ordtresticc  21825  prdsxmetlem  22972  xrge0gsumle  23435  xrge0tsms  23436  metdscn  23458  iccpnfhmeo  23543  xrhmeo  23544  volsup  24151  volsup2  24200  volivth  24202  itg2le  24334  itg2const2  24336  itg2lea  24339  itg2eqa  24340  itg2split  24344  itg2gt0  24355  dvgt0lem1  24593  radcnvlt1  25000  radcnvle  25002  pserulm  25004  psercnlem2  25006  psercnlem1  25007  psercn  25008  pserdvlem1  25009  pserdvlem2  25010  abelthlem3  25015  abelth  25023  logtayl  25237  xrge0infss  30478  xrge0infssd  30479  xrge0subcld  30481  infxrge0lb  30482  infxrge0glb  30483  infxrge0gelb  30484  xrge0base  30667  xrge00  30668  xrge0mulgnn0  30671  xrge0addass  30672  xrge0addgt0  30673  xrge0adddir  30674  xrge0adddi  30675  xrge0npcan  30676  xrge0tsmsd  30687  xrge0slmod  30912  xrge0iifiso  31173  xrge0iifhmeo  31174  xrge0pluscn  31178  xrge0mulc1cn  31179  xrge0tmdALT  31184  lmlimxrge0  31186  pnfneige0  31189  lmxrge0  31190  esummono  31308  esumpad  31309  esumpad2  31310  esumle  31312  gsumesum  31313  esumlub  31314  esumlef  31316  esumcst  31317  esumrnmpt2  31322  esumfsup  31324  esumpinfval  31327  esumpfinvallem  31328  esumpinfsum  31331  esumpmono  31333  esummulc2  31336  esumdivc  31337  hasheuni  31339  esumcvg  31340  esumgect  31344  esum2d  31347  measun  31465  measunl  31470  measiun  31472  voliune  31483  volfiniune  31484  ddemeas  31490  omsfval  31547  omsf  31549  oms0  31550  omssubaddlem  31552  omssubadd  31553  baselcarsg  31559  0elcarsg  31560  difelcarsg  31563  inelcarsg  31564  carsgsigalem  31568  carsggect  31571  carsgclctunlem2  31572  carsgclctunlem3  31573  carsgclctun  31574  omsmeas  31576  pmeasmono  31577  probmeasb  31683  itg2addnclem  34937  ftc1anc  34969  xadd0ge  41581  xrge0nemnfd  41593  xadd0ge2  41602  ge0lere  41801  inficc  41803  iccdificc  41808  fourierdlem1  42387  fourierdlem20  42406  fourierdlem27  42413  fourierdlem87  42472  fge0iccico  42646  gsumge0cl  42647  sge0sn  42655  sge0tsms  42656  sge0xrcl  42661  sge0pr  42670  sge0prle  42677  sge0le  42683  sge0split  42685  sge0p1  42690  sge0rernmpt  42698  sge0xrclmpt  42704  sge0xadd  42711  meaxrcl  42737  meadjun  42738  voliunsge0lem  42748  caragen0  42782  omexrcl  42783  caragenunidm  42784  caragendifcl  42790  omeunle  42792  omeiunle  42793  carageniuncl  42799  ovn0lem  42841  ovnxrcl  42845  hoidmvlelem3  42873  hoidmvlelem4  42874  vonxrcl  42944