Metamath Proof Explorer

Theorem ioorinv2

Description: The function F is an "inverse" of sorts to the open interval function. (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 ioorinv2 
|- ( ( A (,) B ) =/= (/) -> ( F ` ( A (,) B ) ) = <. A , B >. )

Proof

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