Theorem ixxssxr

Description: The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014)

	Ref	Expression
Hypothesis	ixx.1	|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
Assertion	ixxssxr	|- ( A O B ) C_ 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		df-ov	|- ( A O B ) = ( O ` <. A , B >. )
3	1	ixxf	|- O : ( RR* X. RR* ) --> ~P RR*
4		0elpw	|- (/) e. ~P RR*
5	3 4	f0cli	|- ( O ` <. A , B >. ) e. ~P RR*
6	2 5	eqeltri	|- ( A O B ) e. ~P RR*
7		ovex	|- ( A O B ) e. _V
8	7	elpw	|- ( ( A O B ) e. ~P RR* <-> ( A O B ) C_ RR* )
9	6 8	mpbi	|- ( A O B ) C_ RR*