Metamath Proof Explorer

Theorem ioorinv

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 ioorinv 
|- ( A e. ran (,) -> ( (,) ` ( F ` A ) ) = A )

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* ) -> ( A e. ran (,) <-> E. a e. RR* E. b e. RR* A = ( a (,) b ) ) )
5 2 3 4 mp2b 
 |-  ( A e. ran (,) <-> E. a e. RR* E. b e. RR* A = ( a (,) b ) )
6 1 ioorinv2 
 |-  ( ( a (,) b ) =/= (/) -> ( F ` ( a (,) b ) ) = <. a , b >. )
7 6 fveq2d 
 |-  ( ( a (,) b ) =/= (/) -> ( (,) ` ( F ` ( a (,) b ) ) ) = ( (,) ` <. a , b >. ) )
8 df-ov 
 |-  ( a (,) b ) = ( (,) ` <. a , b >. )
9 7 8 eqtr4di 
 |-  ( ( a (,) b ) =/= (/) -> ( (,) ` ( F ` ( a (,) b ) ) ) = ( a (,) b ) )
10 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
11 neeq1 
 |-  ( A = ( a (,) b ) -> ( A =/= (/) <-> ( a (,) b ) =/= (/) ) )
12 10 11 bitr3id 
 |-  ( A = ( a (,) b ) -> ( -. A = (/) <-> ( a (,) b ) =/= (/) ) )
13 2fveq3 
 |-  ( A = ( a (,) b ) -> ( (,) ` ( F ` A ) ) = ( (,) ` ( F ` ( a (,) b ) ) ) )
14 id 
 |-  ( A = ( a (,) b ) -> A = ( a (,) b ) )
15 13 14 eqeq12d 
 |-  ( A = ( a (,) b ) -> ( ( (,) ` ( F ` A ) ) = A <-> ( (,) ` ( F ` ( a (,) b ) ) ) = ( a (,) b ) ) )
16 12 15 imbi12d 
 |-  ( A = ( a (,) b ) -> ( ( -. A = (/) -> ( (,) ` ( F ` A ) ) = A ) <-> ( ( a (,) b ) =/= (/) -> ( (,) ` ( F ` ( a (,) b ) ) ) = ( a (,) b ) ) ) )
17 9 16 mpbiri 
 |-  ( A = ( a (,) b ) -> ( -. A = (/) -> ( (,) ` ( F ` A ) ) = A ) )
18 17 a1i 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( A = ( a (,) b ) -> ( -. A = (/) -> ( (,) ` ( F ` A ) ) = A ) ) )
19 18 rexlimivv 
 |-  ( E. a e. RR* E. b e. RR* A = ( a (,) b ) -> ( -. A = (/) -> ( (,) ` ( F ` A ) ) = A ) )
20 5 19 sylbi 
 |-  ( A e. ran (,) -> ( -. A = (/) -> ( (,) ` ( F ` A ) ) = A ) )
21 ioorebas 
 |-  ( 0 (,) 0 ) e. ran (,)
22 1 ioorval 
 |-  ( ( 0 (,) 0 ) e. ran (,) -> ( F ` ( 0 (,) 0 ) ) = if ( ( 0 (,) 0 ) = (/) , <. 0 , 0 >. , <. inf ( ( 0 (,) 0 ) , RR* , < ) , sup ( ( 0 (,) 0 ) , RR* , < ) >. ) )
23 21 22 ax-mp 
 |-  ( F ` ( 0 (,) 0 ) ) = if ( ( 0 (,) 0 ) = (/) , <. 0 , 0 >. , <. inf ( ( 0 (,) 0 ) , RR* , < ) , sup ( ( 0 (,) 0 ) , RR* , < ) >. )
24 iooid 
 |-  ( 0 (,) 0 ) = (/)
25 24 iftruei 
 |-  if ( ( 0 (,) 0 ) = (/) , <. 0 , 0 >. , <. inf ( ( 0 (,) 0 ) , RR* , < ) , sup ( ( 0 (,) 0 ) , RR* , < ) >. ) = <. 0 , 0 >.
26 23 25 eqtri 
 |-  ( F ` ( 0 (,) 0 ) ) = <. 0 , 0 >.
27 26 fveq2i 
 |-  ( (,) ` ( F ` ( 0 (,) 0 ) ) ) = ( (,) ` <. 0 , 0 >. )
28 df-ov 
 |-  ( 0 (,) 0 ) = ( (,) ` <. 0 , 0 >. )
29 27 28 eqtr4i 
 |-  ( (,) ` ( F ` ( 0 (,) 0 ) ) ) = ( 0 (,) 0 )
30 24 eqeq2i 
 |-  ( A = ( 0 (,) 0 ) <-> A = (/) )
31 30 biimpri 
 |-  ( A = (/) -> A = ( 0 (,) 0 ) )
32 31 fveq2d 
 |-  ( A = (/) -> ( F ` A ) = ( F ` ( 0 (,) 0 ) ) )
33 32 fveq2d 
 |-  ( A = (/) -> ( (,) ` ( F ` A ) ) = ( (,) ` ( F ` ( 0 (,) 0 ) ) ) )
34 29 33 31 3eqtr4a 
 |-  ( A = (/) -> ( (,) ` ( F ` A ) ) = A )
35 20 34 pm2.61d2 
 |-  ( A e. ran (,) -> ( (,) ` ( F ` A ) ) = A )