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

Definition df-ioc 11406
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 11402 . 2  class  (,]
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9518 . . 3  class  RR*
52cv 1369 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1369 . . . . . 6  class  z
8 clt 9519 . . . . . 6  class  <
95, 7, 8wbr 4390 . . . . 5  wff  x  < 
z
103cv 1369 . . . . . 6  class  y
11 cle 9520 . . . . . 6  class  <_
127, 10, 11wbr 4390 . . . . 5  wff  z  <_ 
y
139, 12wa 369 . . . 4  wff  ( x  <  z  /\  z  <_  y )
1413, 6, 4crab 2799 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <_  y ) }
152, 3, 4, 4, 14cmpt2 6192 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
161, 15wceq 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:  iocval  11438  elioc1  11443  iocssxr  11480  snunioc  11514  leordtval2  18932  iocpnfordt  18935  lecldbas  18939  pnfnei  18940  iocmnfcld  20464  xrtgioo  20499  ismbf3d  21248  dvloglem  22209  iocssicc  26193  iocssioo  26195  asindmre  28617  dvasin  28618  ioounsn  29723
  Copyright terms: Public domain W3C validator