Step |
Hyp |
Ref |
Expression |
1 |
|
ioorf.1 |
|- F = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) ) |
2 |
|
ioorebas |
|- ( A (,) B ) e. ran (,) |
3 |
1
|
ioorval |
|- ( ( A (,) B ) e. ran (,) -> ( F ` ( A (,) B ) ) = if ( ( A (,) B ) = (/) , <. 0 , 0 >. , <. inf ( ( A (,) B ) , RR* , < ) , sup ( ( A (,) B ) , RR* , < ) >. ) ) |
4 |
2 3
|
ax-mp |
|- ( F ` ( A (,) B ) ) = if ( ( A (,) B ) = (/) , <. 0 , 0 >. , <. inf ( ( A (,) B ) , RR* , < ) , sup ( ( A (,) B ) , RR* , < ) >. ) |
5 |
|
ifnefalse |
|- ( ( A (,) B ) =/= (/) -> if ( ( A (,) B ) = (/) , <. 0 , 0 >. , <. inf ( ( A (,) B ) , RR* , < ) , sup ( ( A (,) B ) , RR* , < ) >. ) = <. inf ( ( A (,) B ) , RR* , < ) , sup ( ( A (,) B ) , RR* , < ) >. ) |
6 |
|
n0 |
|- ( ( A (,) B ) =/= (/) <-> E. x x e. ( A (,) B ) ) |
7 |
|
eliooxr |
|- ( x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* ) ) |
8 |
7
|
exlimiv |
|- ( E. x x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* ) ) |
9 |
6 8
|
sylbi |
|- ( ( A (,) B ) =/= (/) -> ( A e. RR* /\ B e. RR* ) ) |
10 |
9
|
simpld |
|- ( ( A (,) B ) =/= (/) -> A e. RR* ) |
11 |
9
|
simprd |
|- ( ( A (,) B ) =/= (/) -> B e. RR* ) |
12 |
|
id |
|- ( ( A (,) B ) =/= (/) -> ( A (,) B ) =/= (/) ) |
13 |
|
df-ioo |
|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } ) |
14 |
|
idd |
|- ( ( w e. RR* /\ B e. RR* ) -> ( w < B -> w < B ) ) |
15 |
|
xrltle |
|- ( ( w e. RR* /\ B e. RR* ) -> ( w < B -> w <_ B ) ) |
16 |
|
idd |
|- ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A < w ) ) |
17 |
|
xrltle |
|- ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A <_ w ) ) |
18 |
13 14 15 16 17
|
ixxlb |
|- ( ( A e. RR* /\ B e. RR* /\ ( A (,) B ) =/= (/) ) -> inf ( ( A (,) B ) , RR* , < ) = A ) |
19 |
10 11 12 18
|
syl3anc |
|- ( ( A (,) B ) =/= (/) -> inf ( ( A (,) B ) , RR* , < ) = A ) |
20 |
13 14 15 16 17
|
ixxub |
|- ( ( A e. RR* /\ B e. RR* /\ ( A (,) B ) =/= (/) ) -> sup ( ( A (,) B ) , RR* , < ) = B ) |
21 |
10 11 12 20
|
syl3anc |
|- ( ( A (,) B ) =/= (/) -> sup ( ( A (,) B ) , RR* , < ) = B ) |
22 |
19 21
|
opeq12d |
|- ( ( A (,) B ) =/= (/) -> <. inf ( ( A (,) B ) , RR* , < ) , sup ( ( A (,) B ) , RR* , < ) >. = <. A , B >. ) |
23 |
5 22
|
eqtrd |
|- ( ( A (,) B ) =/= (/) -> if ( ( A (,) B ) = (/) , <. 0 , 0 >. , <. inf ( ( A (,) B ) , RR* , < ) , sup ( ( A (,) B ) , RR* , < ) >. ) = <. A , B >. ) |
24 |
4 23
|
syl5eq |
|- ( ( A (,) B ) =/= (/) -> ( F ` ( A (,) B ) ) = <. A , B >. ) |