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

Definition df-icc 10816
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 10812 . 2  class  [,]
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 9013 . . 3  class  RR*
52cv 1646 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1646 . . . . . 6  class  z
8 cle 9015 . . . . . 6  class  <_
95, 7, 8wbr 4125 . . . . 5  wff  x  <_ 
z
103cv 1646 . . . . . 6  class  y
117, 10, 8wbr 4125 . . . . 5  wff  z  <_ 
y
129, 11wa 358 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2632 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 5983 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1647 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  10848  elicc1  10853  iccss  10871  iccssioo  10872  iccss2  10873  iccssico  10874  iccssxr  10885  ioossicc  10888  iccf  10895  snunioo  10915  snunico  10916  ioodisj  10918  leordtval2  17159  iccordt  17161  lecldbas  17166  ioombl  19137  itg2mulclem  19316  itg2mulc  19317  itgspliticc  19406  psercnlem2  20018  tanord1  20117  icossicc  23529  iocssicc  23530  snunioc  23538  cvmliftlem10  24428  itg2addnc  25677
  Copyright terms: Public domain W3C validator