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