This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ioof

Description: The set of open intervals of extended reals maps to subsets of reals. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Assertion ioof 
|- (,) : ( RR* X. RR* ) --> ~P RR

Proof

Step Hyp Ref Expression
1 iooval 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x (,) y ) = { z e. RR* | ( x < z /\ z < y ) } )
2 ioossre 
 |-  ( x (,) y ) C_ RR
3 ovex 
 |-  ( x (,) y ) e. _V
4 3 elpw 
 |-  ( ( x (,) y ) e. ~P RR <-> ( x (,) y ) C_ RR )
5 2 4 mpbir 
 |-  ( x (,) y ) e. ~P RR
6 1 5 eqeltrrdi 
 |-  ( ( x e. RR* /\ y e. RR* ) -> { z e. RR* | ( x < z /\ z < y ) } e. ~P RR )
7 6 rgen2 
 |-  A. x e. RR* A. y e. RR* { z e. RR* | ( x < z /\ z < y ) } e. ~P RR
8 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
9 8 fmpo 
 |-  ( A. x e. RR* A. y e. RR* { z e. RR* | ( x < z /\ z < y ) } e. ~P RR <-> (,) : ( RR* X. RR* ) --> ~P RR )
10 7 9 mpbi 
 |-  (,) : ( RR* X. RR* ) --> ~P RR