Theorem iccssxr 13561

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

This proof depends on syntax axioms:   ⊆ wss 3895  (class class class)co 7420  ℝ^*cxr 11342   ≤ cle 11344  [,]cicc 13479

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-xr 11347  df-icc 13483

This theorem is used by:  eliccxr  13566  supicclub2  13635  xrge0base  17779  lecldbas  23537  ordtresticc  23541  prdsxmetlem  24687  xrge0gsumle  25153  xrge0tsms  25154  metdscn  25176  iccpnfhmeo  25266  xrhmeo  25267  volsup  25877  volsup2  25926  volivth  25928  itg2le  26060  itg2const2  26062  itg2lea  26065  itg2eqa  26066  itg2split  26070  itg2gt0  26081  dvgt0lem1  26322  radcnvlt1  26745  radcnvle  26747  pserulm  26749  psercnlem2  26751  psercnlem1  26752  psercn  26753  pserdvlem1  26754  pserdvlem2  26755  abelthlem3  26760  abelth  26768  logtayl  26988  xrge0infss  33394  xrge0infssd  33395  xrge0subcld  33397  infxrge0lb  33398  infxrge0glb  33399  infxrge0gelb  33400  xrge00  33617  xrge0mulgnn0  33618  xrge0addass  33619  xrge0addgt0  33620  xrge0adddir  33621  xrge0adddi  33622  xrge0npcan  33623  xrge0tsmsd  33676  xrge0slmod  33951  xrge0iifiso  34609  xrge0iifhmeo  34610  xrge0pluscn  34614  xrge0mulc1cn  34615  xrge0tmdALT  34620  lmlimxrge0  34622  pnfneige0  34625  lmxrge0  34626  esummono  34728  esumpad  34729  esumpad2  34730  esumle  34732  gsumesum  34733  esumlub  34734  esumlef  34736  esumcst  34737  esumrnmpt2  34742  esumfsup  34744  esumpinfval  34747  esumpfinvallem  34748  esumpinfsum  34751  esumpmono  34753  esummulc2  34756  esumdivc  34757  hasheuni  34759  esumcvg  34760  esumgect  34764  esum2d  34767  measun  34886  measunl  34891  measiun  34893  voliune  34904  volfiniune  34905  ddemeas  34911  omsfval  34968  omsf  34970  oms0  34971  omssubaddlem  34973  omssubadd  34974  baselcarsg  34980  0elcarsg  34981  difelcarsg  34984  inelcarsg  34985  carsgsigalem  34989  carsggect  34992  carsgclctunlem2  34993  carsgclctunlem3  34994  carsgclctun  34995  omsmeas  34997  pmeasmono  34998  probmeasb  35104  itg2addnclem  38632  ftc1anc  38662  xadd0ge  46377  xrge0nemnfd  46387  xadd0ge2  46396  ge0lere  46587  inficc  46589  iccdificc  46594  fourierdlem1  47161  fourierdlem20  47180  fourierdlem27  47187  fourierdlem87  47246  fge0iccico  47423  gsumge0cl  47424  sge0sn  47432  sge0tsms  47433  sge0xrcl  47438  sge0pr  47447  sge0prle  47454  sge0le  47460  sge0split  47462  sge0p1  47467  sge0rernmpt  47475  sge0xrclmpt  47481  sge0xadd  47488  meaxrcl  47514  meadjun  47515  voliunsge0lem  47525  caragen0  47559  omexrcl  47560  caragenunidm  47561  caragendifcl  47567  omeunle  47569  omeiunle  47570  carageniuncl  47576  ovn0lem  47618  ovnxrcl  47622  hoidmvlelem3  47650  hoidmvlelem4  47651  vonxrcl  47721  icccldii  50070