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*