Theorem icoreelrn

Description: A class abstraction which is an element of the set of closed-below, open-above intervals of reals. (Contributed by ML, 1-Aug-2020)

	Ref	Expression
Hypothesis	icoreelrn.1	|- I = ( [,) " ( RR X. RR ) )
Assertion	icoreelrn	|- ( ( A e. RR /\ B e. RR ) -> { z e. RR | ( A <_ z /\ z < B ) } e. I )

Proof

Step	Hyp	Ref	Expression
1		icoreelrn.1	|- I = ( [,) " ( RR X. RR ) )
2		icoreval	|- ( ( A e. RR /\ B e. RR ) -> ( A [,) B ) = { z e. RR | ( A <_ z /\ z < B ) } )
3		simpl	|- ( ( A e. RR /\ B e. RR ) -> A e. RR )
4		simpr	|- ( ( A e. RR /\ B e. RR ) -> B e. RR )
5		df-ico	|- [,) = ( a e. RR* , b e. RR* |-> { z e. RR* | ( a <_ z /\ z < b ) } )
6	5	ixxf	|- [,) : ( RR* X. RR* ) --> ~P RR*
7		ffun	|- ( [,) : ( RR* X. RR* ) --> ~P RR* -> Fun [,) )
8	6 7	mp1i	|- ( ( A e. RR /\ B e. RR ) -> Fun [,) )
9		rexpssxrxp	|- ( RR X. RR ) C_ ( RR* X. RR* )
10	6	fdmi	|- dom [,) = ( RR* X. RR* )
11	9 10	sseqtrri	|- ( RR X. RR ) C_ dom [,)
12	11	a1i	|- ( ( A e. RR /\ B e. RR ) -> ( RR X. RR ) C_ dom [,) )
13	3 4 8 12	elovimad	|- ( ( A e. RR /\ B e. RR ) -> ( A [,) B ) e. ( [,) " ( RR X. RR ) ) )
14	13 1	eleqtrrdi	|- ( ( A e. RR /\ B e. RR ) -> ( A [,) B ) e. I )
15	2 14	eqeltrrd	|- ( ( A e. RR /\ B e. RR ) -> { z e. RR | ( A <_ z /\ z < B ) } e. I )