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

Definition df-icc 11421
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 11417 . 2  class  [,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9531 . . 3  class  RR*
52cv 1369 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1369 . . . . . 6  class  z
8 cle 9533 . . . . . 6  class  <_
95, 7, 8wbr 4403 . . . . 5  wff  x  <_ 
z
103cv 1369 . . . . . 6  class  y
117, 10, 8wbr 4403 . . . . 5  wff  z  <_ 
y
129, 11wa 369 . . . 4  wff  ( x  <_  z  /\  z  <_  y )
1312, 6, 4crab 2803 . . 3  class  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) }
142, 3, 4, 4, 13cmpt2 6205 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
151, 14wceq 1370 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  11453  elicc1  11458  iccss  11477  iccssioo  11478  iccss2  11480  iccssico  11481  iccssxr  11492  ioossicc  11495  icossicc  11496  iocssicc  11497  iccf  11508  snunioo  11531  snunico  11532  snunioc  11533  ioodisj  11535  leordtval2  18951  iccordt  18953  lecldbas  18958  ioombl  21182  itg2mulclem  21360  itg2mulc  21361  itgspliticc  21450  psercnlem2  22025  tanord1  22129  cvmliftlem10  27347  ftc1anclem7  28641  ftc1anclem8  28642  ftc1anc  28643  ioounsn  29753
  Copyright terms: Public domain W3C validator