MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-icc Unicode version

Definition df-icc 10912
Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-icc  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-icc
StepHypRef Expression
1 cicc 10908 . 2  class  [,]
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9108 . . 3  class  RR*
52cv 1651 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1651 . . . . . 6  class  z
8 cle 9110 . . . . . 6  class  <_
95, 7, 8wbr 4204 . . . . 5  wff  x  <_ 
z
103cv 1651 . . . . . 6  class  y
117, 10, 8wbr 4204 . . . . 5  wff  z  <_ 
y
129, 11wa 359 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2701 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6074 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1652 1  wff  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
Colors of variables: wff set class
This definition is referenced by:  iccval  10944  elicc1  10949  iccss  10967  iccssioo  10968  iccss2  10970  iccssico  10971  iccssxr  10982  ioossicc  10985  iccf  10992  snunioo  11012  snunico  11013  ioodisj  11015  leordtval2  17264  iccordt  17266  lecldbas  17271  ioombl  19447  itg2mulclem  19626  itg2mulc  19627  itgspliticc  19716  psercnlem2  20328  tanord1  20427  icossicc  24117  iocssicc  24118  snunioc  24125  cvmliftlem10  24969
  Copyright terms: Public domain W3C validator