Metamath Proof Explorer


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 )