Theorem ixxex

Description: The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Hypothesis	ixx.1	|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
Assertion	ixxex	|- O e. _V

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	2 2	xpex	|- ( RR* X. RR* ) e. _V
4	2	pwex	|- ~P RR* e. _V
5	3 4	xpex	|- ( ( RR* X. RR* ) X. ~P RR* ) e. _V
6	1	ixxf	|- O : ( RR* X. RR* ) --> ~P RR*
7		fssxp	|- ( O : ( RR* X. RR* ) --> ~P RR* -> O C_ ( ( RR* X. RR* ) X. ~P RR* ) )
8	6 7	ax-mp	|- O C_ ( ( RR* X. RR* ) X. ~P RR* )
9	5 8	ssexi	|- O e. _V