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