Theorem iccssxr 13588

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

This proof depends on syntax axioms:   ⊆ wss 3900  (class class class)co 7443  ℝ^*cxr 11369   ≤ cle 11371  [,]cicc 13506

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-1st 8025  df-2nd 8026  df-xr 11374  df-icc 13510

This theorem is used by:  eliccxr  13593  supicclub2  13662  xrge0base  17808  lecldbas  23567  ordtresticc  23571  prdsxmetlem  24717  xrge0gsumle  25183  xrge0tsms  25184  metdscn  25206  iccpnfhmeo  25296  xrhmeo  25297  volsup  25907  volsup2  25956  volivth  25958  itg2le  26090  itg2const2  26092  itg2lea  26095  itg2eqa  26096  itg2split  26100  itg2gt0  26111  dvgt0lem1  26352  radcnvlt1  26775  radcnvle  26777  pserulm  26779  psercnlem2  26781  psercnlem1  26782  psercn  26783  pserdvlem1  26784  pserdvlem2  26785  abelthlem3  26790  abelth  26798  logtayl  27018  xrge0infss  33422  xrge0infssd  33423  xrge0subcld  33425  infxrge0lb  33426  infxrge0glb  33427  infxrge0gelb  33428  xrge00  33645  xrge0mulgnn0  33646  xrge0addass  33647  xrge0addgt0  33648  xrge0adddir  33649  xrge0adddi  33650  xrge0npcan  33651  xrge0tsmsd  33704  xrge0slmod  33979  xrge0iifiso  34637  xrge0iifhmeo  34638  xrge0pluscn  34642  xrge0mulc1cn  34643  xrge0tmdALT  34648  lmlimxrge0  34650  pnfneige0  34653  lmxrge0  34654  esummono  34756  esumpad  34757  esumpad2  34758  esumle  34760  gsumesum  34761  esumlub  34762  esumlef  34764  esumcst  34765  esumrnmpt2  34770  esumfsup  34772  esumpinfval  34775  esumpfinvallem  34776  esumpinfsum  34779  esumpmono  34781  esummulc2  34784  esumdivc  34785  hasheuni  34787  esumcvg  34788  esumgect  34792  esum2d  34795  measun  34914  measunl  34919  measiun  34921  voliune  34932  volfiniune  34933  ddemeas  34939  omsfval  34996  omsf  34998  oms0  34999  omssubaddlem  35001  omssubadd  35002  baselcarsg  35008  0elcarsg  35009  difelcarsg  35012  inelcarsg  35013  carsgsigalem  35017  carsggect  35020  carsgclctunlem2  35021  carsgclctunlem3  35022  carsgclctun  35023  omsmeas  35025  pmeasmono  35026  probmeasb  35132  itg2addnclem  38781  ftc1anc  38811  xadd0ge  46539  xrge0nemnfd  46549  xadd0ge2  46558  ge0lere  46749  inficc  46751  iccdificc  46756  fourierdlem1  47323  fourierdlem20  47342  fourierdlem27  47349  fourierdlem87  47408  fge0iccico  47585  gsumge0cl  47586  sge0sn  47594  sge0tsms  47595  sge0xrcl  47600  sge0pr  47609  sge0prle  47616  sge0le  47622  sge0split  47624  sge0p1  47629  sge0rernmpt  47637  sge0xrclmpt  47643  sge0xadd  47650  meaxrcl  47676  meadjun  47677  voliunsge0lem  47687  caragen0  47721  omexrcl  47722  caragenunidm  47723  caragendifcl  47729  omeunle  47731  omeiunle  47732  carageniuncl  47738  ovn0lem  47780  ovnxrcl  47784  hoidmvlelem3  47812  hoidmvlelem4  47813  vonxrcl  47883  icccldii  50238