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* |
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* |