Metamath Proof Explorer


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*