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