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

Definition df-icc 11642
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 11638 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9674 . . 3  class  RR*
52cv 1443 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1443 . . . . . 6  class  z
8 cle 9676 . . . . . 6  class  <_
95, 7, 8wbr 4402 . . . . 5  wff  x  <_ 
z
103cv 1443 . . . . . 6  class  y
117, 10, 8wbr 4402 . . . . 5  wff  z  <_ 
y
129, 11wa 371 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2741 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6292 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1444 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  11675  elicc1  11680  iccss  11702  iccssioo  11703  iccss2  11705  iccssico  11706  iccssxr  11717  ioossicc  11720  icossicc  11721  iocssicc  11722  iccf  11733  snunioo  11758  snunico  11759  snunioc  11760  ioodisj  11762  leordtval2  20228  iccordt  20230  lecldbas  20235  ioombl  22518  itgspliticc  22794  psercnlem2  23379  tanord1  23486  cvmliftlem10  30017  ftc1anclem7  32023  ftc1anclem8  32024  ftc1anc  32025  ioounsn  36094  snunioo2  37606  snunioo1  37613
  Copyright terms: Public domain W3C validator