This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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*