Metamath Proof Explorer


Definition df-ioo

Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006)

Ref Expression
Assertion df-ioo
|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cioo
 |-  (,)
1 vx
 |-  x
2 cxr
 |-  RR*
3 vy
 |-  y
4 vz
 |-  z
5 1 cv
 |-  x
6 clt
 |-  <
7 4 cv
 |-  z
8 5 7 6 wbr
 |-  x < z
9 3 cv
 |-  y
10 7 9 6 wbr
 |-  z < y
11 8 10 wa
 |-  ( x < z /\ z < y )
12 11 4 2 crab
 |-  { z e. RR* | ( x < z /\ z < y ) }
13 1 3 2 2 12 cmpo
 |-  ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
14 0 13 wceq
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )