Theorem iccssxr 13444

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

Syntax hints:   ⊆ wss 3905  (class class class)co 7396  ℝ^*cxr 11226   ≤ cle 11228  [,]cicc 13362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7718  ax-cnex 11140  ax-resscn 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-xr 11231  df-icc 13366

This theorem is referenced by:  eliccxr  13449  supicclub2  13518  xrge0base  17647  lecldbas  23286  ordtresticc  23290  prdsxmetlem  24435  xrge0gsumle  24901  xrge0tsms  24902  metdscn  24924  iccpnfhmeo  25014  xrhmeo  25015  volsup  25625  volsup2  25674  volivth  25676  itg2le  25808  itg2const2  25810  itg2lea  25813  itg2eqa  25814  itg2split  25818  itg2gt0  25829  dvgt0lem1  26071  radcnvlt1  26488  radcnvle  26490  pserulm  26492  psercnlem2  26494  psercnlem1  26495  psercn  26496  pserdvlem1  26497  pserdvlem2  26498  abelthlem3  26503  abelth  26511  logtayl  26732  xrge0infss  32968  xrge0infssd  32969  xrge0subcld  32971  infxrge0lb  32972  infxrge0glb  32973  infxrge0gelb  32974  xrge00  33198  xrge0mulgnn0  33199  xrge0addass  33200  xrge0addgt0  33201  xrge0adddir  33202  xrge0adddi  33203  xrge0npcan  33204  xrge0tsmsd  33259  xrge0slmod  33537  xrge0iifiso  34234  xrge0iifhmeo  34235  xrge0pluscn  34239  xrge0mulc1cn  34240  xrge0tmdALT  34245  lmlimxrge0  34247  pnfneige0  34250  lmxrge0  34251  esummono  34353  esumpad  34354  esumpad2  34355  esumle  34357  gsumesum  34358  esumlub  34359  esumlef  34361  esumcst  34362  esumrnmpt2  34367  esumfsup  34369  esumpinfval  34372  esumpfinvallem  34373  esumpinfsum  34376  esumpmono  34378  esummulc2  34381  esumdivc  34382  hasheuni  34384  esumcvg  34385  esumgect  34389  esum2d  34392  measun  34510  measunl  34515  measiun  34517  voliune  34528  volfiniune  34529  ddemeas  34535  omsfval  34593  omsf  34595  oms0  34596  omssubaddlem  34598  omssubadd  34599  baselcarsg  34605  0elcarsg  34606  difelcarsg  34609  inelcarsg  34610  carsgsigalem  34614  carsggect  34617  carsgclctunlem2  34618  carsgclctunlem3  34619  carsgclctun  34620  omsmeas  34622  pmeasmono  34623  probmeasb  34729  itg2addnclem  38175  ftc1anc  38205  xadd0ge  45889  xrge0nemnfd  45899  xadd0ge2  45908  ge0lere  46099  inficc  46101  iccdificc  46106  fourierdlem1  46673  fourierdlem20  46692  fourierdlem27  46699  fourierdlem87  46758  fge0iccico  46935  gsumge0cl  46936  sge0sn  46944  sge0tsms  46945  sge0xrcl  46950  sge0pr  46959  sge0prle  46966  sge0le  46972  sge0split  46974  sge0p1  46979  sge0rernmpt  46987  sge0xrclmpt  46993  sge0xadd  47000  meaxrcl  47026  meadjun  47027  voliunsge0lem  47037  caragen0  47071  omexrcl  47072  caragenunidm  47073  caragendifcl  47079  omeunle  47081  omeiunle  47082  carageniuncl  47088  ovn0lem  47130  ovnxrcl  47134  hoidmvlelem3  47162  hoidmvlelem4  47163  vonxrcl  47233  icccldii  49531