MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iccssxr Structured version   Unicode version

Theorem iccssxr 11482
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  |-  ( A [,] B )  C_  RR*

Proof of Theorem iccssxr
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-icc 11411 . 2  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
21ixxssxr 11416 1  |-  ( A [,] B )  C_  RR*
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3429  (class class class)co 6193   RR*cxr 9521    <_ cle 9523   [,]cicc 11407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-cnex 9442  ax-resscn 9443
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-fv 5527  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-1st 6680  df-2nd 6681  df-xr 9526  df-icc 11411
This theorem is referenced by:  supicclub2  11546  lecldbas  18948  ordtresticc  18952  prdsxmetlem  20068  xrge0gsumle  20535  xrge0tsms  20536  metdscn  20557  iccpnfhmeo  20642  xrhmeo  20643  volsup  21163  volsup2  21211  volivth  21213  itg2le  21343  itg2const2  21345  itg2lea  21348  itg2eqa  21349  itg2split  21353  itg2gt0  21364  dvgt0lem1  21600  radcnvlt1  22009  radcnvle  22011  pserulm  22013  psercnlem2  22015  psercnlem1  22016  psercn  22017  pserdvlem1  22018  pserdvlem2  22019  abelthlem3  22024  abelth  22032  logtayl  22231  xrge0infss  26197  xrge0infssd  26198  xrge0base  26284  xrge00  26285  xrge0mulgnn0  26288  xrge0addass  26289  xrge0nre  26291  xrge0addgt0  26292  xrge0adddir  26293  xrge0adddi  26294  xrge0npcan  26295  xrge0omnd  26312  xrge0tsmsd  26391  xrge0slmod  26450  xrge0iifiso  26503  xrge0iifhmeo  26504  xrge0pluscn  26508  xrge0mulc1cn  26509  xrge0tmdOLD  26513  lmlimxrge0  26516  pnfneige0  26519  lmxrge0  26520  esumle  26646  esummono  26647  gsumesum  26648  esumlub  26649  esumlef  26651  esumcst  26652  esumfsup  26657  esumpinfval  26660  esumpfinvallem  26661  esumpinfsum  26664  esumpmono  26666  esummulc2  26669  esumdivc  26670  hasheuni  26672  esumcvg  26673  measun  26763  measunl  26768  measiun  26770  voliune  26782  volfiniune  26783  ddemeas  26789  omsfval  26846  oms0  26847  probmeasb  26950  mblfinlem1  28569  itg2addnclem  28584  ftc1anc  28616
  Copyright terms: Public domain W3C validator