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