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

Definition df-icc 11589
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 11585 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9657 . . 3  class  RR*
52cv 1404 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1404 . . . . . 6  class  z
8 cle 9659 . . . . . 6  class  <_
95, 7, 8wbr 4395 . . . . 5  wff  x  <_ 
z
103cv 1404 . . . . . 6  class  y
117, 10, 8wbr 4395 . . . . 5  wff  z  <_ 
y
129, 11wa 367 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2758 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6280 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1405 1  wff  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
Colors of variables: wff setvar class
This definition is referenced by:  iccval  11621  elicc1  11626  iccss  11646  iccssioo  11647  iccss2  11649  iccssico  11650  iccssxr  11661  ioossicc  11664  icossicc  11665  iocssicc  11666  iccf  11677  snunioo  11700  snunico  11701  snunioc  11702  ioodisj  11704  leordtval2  20006  iccordt  20008  lecldbas  20013  ioombl  22267  itgspliticc  22535  psercnlem2  23111  tanord1  23216  cvmliftlem10  29591  ftc1anclem7  31469  ftc1anclem8  31470  ftc1anc  31471  ioounsn  35541  snunioo2  36912  snunioo1  36920
  Copyright terms: Public domain W3C validator