Step |
Hyp |
Ref |
Expression |
1 |
|
ioorf.1 |
|- F = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) ) |
2 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
3 |
|
ffn |
|- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) ) |
4 |
|
ovelrn |
|- ( (,) Fn ( RR* X. RR* ) -> ( x e. ran (,) <-> E. a e. RR* E. b e. RR* x = ( a (,) b ) ) ) |
5 |
2 3 4
|
mp2b |
|- ( x e. ran (,) <-> E. a e. RR* E. b e. RR* x = ( a (,) b ) ) |
6 |
|
0le0 |
|- 0 <_ 0 |
7 |
|
df-br |
|- ( 0 <_ 0 <-> <. 0 , 0 >. e. <_ ) |
8 |
6 7
|
mpbi |
|- <. 0 , 0 >. e. <_ |
9 |
|
0xr |
|- 0 e. RR* |
10 |
|
opelxpi |
|- ( ( 0 e. RR* /\ 0 e. RR* ) -> <. 0 , 0 >. e. ( RR* X. RR* ) ) |
11 |
9 9 10
|
mp2an |
|- <. 0 , 0 >. e. ( RR* X. RR* ) |
12 |
8 11
|
elini |
|- <. 0 , 0 >. e. ( <_ i^i ( RR* X. RR* ) ) |
13 |
12
|
a1i |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ x = (/) ) -> <. 0 , 0 >. e. ( <_ i^i ( RR* X. RR* ) ) ) |
14 |
|
simplr |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> x = ( a (,) b ) ) |
15 |
14
|
infeq1d |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> inf ( x , RR* , < ) = inf ( ( a (,) b ) , RR* , < ) ) |
16 |
|
simplll |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> a e. RR* ) |
17 |
|
simpllr |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> b e. RR* ) |
18 |
|
simpr |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> -. x = (/) ) |
19 |
18
|
neqned |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> x =/= (/) ) |
20 |
14 19
|
eqnetrrd |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> ( a (,) b ) =/= (/) ) |
21 |
|
df-ioo |
|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } ) |
22 |
|
idd |
|- ( ( w e. RR* /\ b e. RR* ) -> ( w < b -> w < b ) ) |
23 |
|
xrltle |
|- ( ( w e. RR* /\ b e. RR* ) -> ( w < b -> w <_ b ) ) |
24 |
|
idd |
|- ( ( a e. RR* /\ w e. RR* ) -> ( a < w -> a < w ) ) |
25 |
|
xrltle |
|- ( ( a e. RR* /\ w e. RR* ) -> ( a < w -> a <_ w ) ) |
26 |
21 22 23 24 25
|
ixxlb |
|- ( ( a e. RR* /\ b e. RR* /\ ( a (,) b ) =/= (/) ) -> inf ( ( a (,) b ) , RR* , < ) = a ) |
27 |
16 17 20 26
|
syl3anc |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> inf ( ( a (,) b ) , RR* , < ) = a ) |
28 |
15 27
|
eqtrd |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> inf ( x , RR* , < ) = a ) |
29 |
14
|
supeq1d |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> sup ( x , RR* , < ) = sup ( ( a (,) b ) , RR* , < ) ) |
30 |
21 22 23 24 25
|
ixxub |
|- ( ( a e. RR* /\ b e. RR* /\ ( a (,) b ) =/= (/) ) -> sup ( ( a (,) b ) , RR* , < ) = b ) |
31 |
16 17 20 30
|
syl3anc |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> sup ( ( a (,) b ) , RR* , < ) = b ) |
32 |
29 31
|
eqtrd |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> sup ( x , RR* , < ) = b ) |
33 |
28 32
|
opeq12d |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. = <. a , b >. ) |
34 |
|
ioon0 |
|- ( ( a e. RR* /\ b e. RR* ) -> ( ( a (,) b ) =/= (/) <-> a < b ) ) |
35 |
34
|
ad2antrr |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> ( ( a (,) b ) =/= (/) <-> a < b ) ) |
36 |
20 35
|
mpbid |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> a < b ) |
37 |
|
xrltle |
|- ( ( a e. RR* /\ b e. RR* ) -> ( a < b -> a <_ b ) ) |
38 |
37
|
ad2antrr |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> ( a < b -> a <_ b ) ) |
39 |
36 38
|
mpd |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> a <_ b ) |
40 |
|
df-br |
|- ( a <_ b <-> <. a , b >. e. <_ ) |
41 |
39 40
|
sylib |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> <. a , b >. e. <_ ) |
42 |
|
opelxpi |
|- ( ( a e. RR* /\ b e. RR* ) -> <. a , b >. e. ( RR* X. RR* ) ) |
43 |
42
|
ad2antrr |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> <. a , b >. e. ( RR* X. RR* ) ) |
44 |
41 43
|
elind |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> <. a , b >. e. ( <_ i^i ( RR* X. RR* ) ) ) |
45 |
33 44
|
eqeltrd |
|- ( ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) /\ -. x = (/) ) -> <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. e. ( <_ i^i ( RR* X. RR* ) ) ) |
46 |
13 45
|
ifclda |
|- ( ( ( a e. RR* /\ b e. RR* ) /\ x = ( a (,) b ) ) -> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) e. ( <_ i^i ( RR* X. RR* ) ) ) |
47 |
46
|
ex |
|- ( ( a e. RR* /\ b e. RR* ) -> ( x = ( a (,) b ) -> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) e. ( <_ i^i ( RR* X. RR* ) ) ) ) |
48 |
47
|
rexlimivv |
|- ( E. a e. RR* E. b e. RR* x = ( a (,) b ) -> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) e. ( <_ i^i ( RR* X. RR* ) ) ) |
49 |
5 48
|
sylbi |
|- ( x e. ran (,) -> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) e. ( <_ i^i ( RR* X. RR* ) ) ) |
50 |
1 49
|
fmpti |
|- F : ran (,) --> ( <_ i^i ( RR* X. RR* ) ) |