Metamath Proof Explorer


Theorem iooex

Description: The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion iooex .V

Proof

Step Hyp Ref Expression
1 df-ioo .=x*,y*z*|x<zz<y
2 1 ixxex .V