Theorem ixxf

Description: The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007) (Revised by Mario Carneiro, 16-Nov-2013)

	Ref	Expression
Hypothesis	ixx.1	|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
Assertion	ixxf	|- O : ( RR* X. RR* ) --> ~P RR*

Proof

Step	Hyp	Ref	Expression
1		ixx.1	|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
2		xrex	|- RR* e. _V
3		ssrab2	|- { z e. RR* | ( x R z /\ z S y ) } C_ RR*
4	2 3	elpwi2	|- { z e. RR* | ( x R z /\ z S y ) } e. ~P RR*
5	4	rgen2w	|- A. x e. RR* A. y e. RR* { z e. RR* | ( x R z /\ z S y ) } e. ~P RR*
6	1	fmpo	|- ( A. x e. RR* A. y e. RR* { z e. RR* | ( x R z /\ z S y ) } e. ~P RR* <-> O : ( RR* X. RR* ) --> ~P RR* )
7	5 6	mpbi	|- O : ( RR* X. RR* ) --> ~P RR*