Metamath Proof Explorer


Theorem icof

Description: The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion icof
|- [,) : ( RR* X. RR* ) --> ~P RR*

Proof

Step Hyp Ref Expression
1 eqidd
 |-  ( ( x e. RR* /\ y e. RR* ) -> { z e. RR* | ( x <_ z /\ z < y ) } = { z e. RR* | ( x <_ z /\ z < y ) } )
2 ssrab2
 |-  { z e. RR* | ( x <_ z /\ z < y ) } C_ RR*
3 xrex
 |-  RR* e. _V
4 3 rabex
 |-  { z e. RR* | ( x <_ z /\ z < y ) } e. _V
5 4 elpw
 |-  ( { z e. RR* | ( x <_ z /\ z < y ) } e. ~P RR* <-> { z e. RR* | ( x <_ z /\ z < y ) } C_ RR* )
6 2 5 mpbir
 |-  { z e. RR* | ( x <_ z /\ z < y ) } e. ~P RR*
7 1 6 eqeltrrdi
 |-  ( ( x e. RR* /\ y e. RR* ) -> { z e. RR* | ( x <_ z /\ z < y ) } e. ~P RR* )
8 7 rgen2
 |-  A. x e. RR* A. y e. RR* { z e. RR* | ( x <_ z /\ z < y ) } e. ~P RR*
9 df-ico
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
10 9 fmpo
 |-  ( A. x e. RR* A. y e. RR* { z e. RR* | ( x <_ z /\ z < y ) } e. ~P RR* <-> [,) : ( RR* X. RR* ) --> ~P RR* )
11 8 10 mpbi
 |-  [,) : ( RR* X. RR* ) --> ~P RR*