Metamath Proof Explorer

Theorem ioorf

Description: Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypothesis ioorf.1 
|- F = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) )
Assertion ioorf 
|- F : ran (,) --> ( <_ i^i ( RR* X. RR* ) )

Proof

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