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

Definition df-ioc 11455
Description: Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioc  |-  (,]  =  ( 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-ioc
StepHypRef Expression
1 cioc 11451 . 2  class  (,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9538 . . 3  class  RR*
52cv 1398 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1398 . . . . . 6  class  z
8 clt 9539 . . . . . 6  class  <
95, 7, 8wbr 4367 . . . . 5  wff  x  < 
z
103cv 1398 . . . . . 6  class  y
11 cle 9540 . . . . . 6  class  <_
127, 10, 11wbr 4367 . . . . 5  wff  z  <_ 
y
139, 12wa 367 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2736 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 6198 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 1399 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:  iocval  11487  elioc1  11492  iocssxr  11529  iocssicc  11533  iocssioo  11535  snunioc  11569  leordtval2  19799  iocpnfordt  19802  lecldbas  19806  pnfnei  19807  iocmnfcld  21361  xrtgioo  21396  ismbf3d  22146  dvloglem  23116  asindmre  30268  dvasin  30269  ioounsn  31345  ioossioc  31690  snunioo2  31710  eliocre  31713  lbioc  31719
  Copyright terms: Public domain W3C validator