Theorem iccssxr 13530

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

This proof depends on syntax axioms:   ⊆ wss 3898  (class class class)co 7408  ℝ^*cxr 11313   ≤ cle 11315  [,]cicc 13448

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734  ax-cnex 11227  ax-resscn 11228

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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-dif 3901  df-un 3903  df-in 3905  df-ss 3915  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 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-fv 6535  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7984  df-2nd 7985  df-xr 11318  df-icc 13452

This theorem is used by:  eliccxr  13535  supicclub2  13604  xrge0base  17740  lecldbas  23498  ordtresticc  23502  prdsxmetlem  24648  xrge0gsumle  25114  xrge0tsms  25115  metdscn  25137  iccpnfhmeo  25227  xrhmeo  25228  volsup  25838  volsup2  25887  volivth  25889  itg2le  26021  itg2const2  26023  itg2lea  26026  itg2eqa  26027  itg2split  26031  itg2gt0  26042  dvgt0lem1  26283  radcnvlt1  26708  radcnvle  26710  pserulm  26712  psercnlem2  26714  psercnlem1  26715  psercn  26716  pserdvlem1  26717  pserdvlem2  26718  abelthlem3  26723  abelth  26731  logtayl  26951  xrge0infss  33285  xrge0infssd  33286  xrge0subcld  33288  infxrge0lb  33289  infxrge0glb  33290  infxrge0gelb  33291  xrge00  33508  xrge0mulgnn0  33509  xrge0addass  33510  xrge0addgt0  33511  xrge0adddir  33512  xrge0adddi  33513  xrge0npcan  33514  xrge0tsmsd  33567  xrge0slmod  33842  xrge0iifiso  34500  xrge0iifhmeo  34501  xrge0pluscn  34505  xrge0mulc1cn  34506  xrge0tmdALT  34511  lmlimxrge0  34513  pnfneige0  34516  lmxrge0  34517  esummono  34619  esumpad  34620  esumpad2  34621  esumle  34623  gsumesum  34624  esumlub  34625  esumlef  34627  esumcst  34628  esumrnmpt2  34633  esumfsup  34635  esumpinfval  34638  esumpfinvallem  34639  esumpinfsum  34642  esumpmono  34644  esummulc2  34647  esumdivc  34648  hasheuni  34650  esumcvg  34651  esumgect  34655  esum2d  34658  measun  34777  measunl  34782  measiun  34784  voliune  34795  volfiniune  34796  ddemeas  34802  omsfval  34860  omsf  34862  oms0  34863  omssubaddlem  34865  omssubadd  34866  baselcarsg  34872  0elcarsg  34873  difelcarsg  34876  inelcarsg  34877  carsgsigalem  34881  carsggect  34884  carsgclctunlem2  34885  carsgclctunlem3  34886  carsgclctun  34887  omsmeas  34889  pmeasmono  34890  probmeasb  34996  itg2addnclem  38509  ftc1anc  38539  xadd0ge  46256  xrge0nemnfd  46266  xadd0ge2  46275  ge0lere  46466  inficc  46468  iccdificc  46473  fourierdlem1  47040  fourierdlem20  47059  fourierdlem27  47066  fourierdlem87  47125  fge0iccico  47302  gsumge0cl  47303  sge0sn  47311  sge0tsms  47312  sge0xrcl  47317  sge0pr  47326  sge0prle  47333  sge0le  47339  sge0split  47341  sge0p1  47346  sge0rernmpt  47354  sge0xrclmpt  47360  sge0xadd  47367  meaxrcl  47393  meadjun  47394  voliunsge0lem  47404  caragen0  47438  omexrcl  47439  caragenunidm  47440  caragendifcl  47446  omeunle  47448  omeiunle  47449  carageniuncl  47455  ovn0lem  47497  ovnxrcl  47501  hoidmvlelem3  47529  hoidmvlelem4  47530  vonxrcl  47600  icccldii  49949