Metamath Proof Explorer

Theorem ioorcl

Description: The function F does not always return real numbers, but it does on intervals of finite volume. (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 ioorcl 
|- ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) -> ( F ` A ) e. ( <_ 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 1 ioorf 
 |-  F : ran (,) --> ( <_ i^i ( RR* X. RR* ) )
3 2 ffvelrni 
 |-  ( A e. ran (,) -> ( F ` A ) e. ( <_ i^i ( RR* X. RR* ) ) )
4 3 adantr 
 |-  ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) -> ( F ` A ) e. ( <_ i^i ( RR* X. RR* ) ) )
5 4 elin1d 
 |-  ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) -> ( F ` A ) e. <_ )
6 1 ioorval 
 |-  ( A e. ran (,) -> ( F ` A ) = if ( A = (/) , <. 0 , 0 >. , <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. ) )
7 6 adantr 
 |-  ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) -> ( F ` A ) = if ( A = (/) , <. 0 , 0 >. , <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. ) )
8 iftrue 
 |-  ( A = (/) -> if ( A = (/) , <. 0 , 0 >. , <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. ) = <. 0 , 0 >. )
9 7 8 sylan9eq 
 |-  ( ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) /\ A = (/) ) -> ( F ` A ) = <. 0 , 0 >. )
10 0re 
 |-  0 e. RR
11 opelxpi 
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> <. 0 , 0 >. e. ( RR X. RR ) )
12 10 10 11 mp2an 
 |-  <. 0 , 0 >. e. ( RR X. RR )
13 9 12 eqeltrdi 
 |-  ( ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) /\ A = (/) ) -> ( F ` A ) e. ( RR X. RR ) )
14 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
15 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
16 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( A e. ran (,) <-> E. a e. RR* E. b e. RR* A = ( a (,) b ) ) )
17 14 15 16 mp2b 
 |-  ( A e. ran (,) <-> E. a e. RR* E. b e. RR* A = ( a (,) b ) )
18 1 ioorinv2 
 |-  ( ( a (,) b ) =/= (/) -> ( F ` ( a (,) b ) ) = <. a , b >. )
19 18 adantl 
 |-  ( ( ( vol* ` ( a (,) b ) ) e. RR /\ ( a (,) b ) =/= (/) ) -> ( F ` ( a (,) b ) ) = <. a , b >. )
20 ioorcl2 
 |-  ( ( ( a (,) b ) =/= (/) /\ ( vol* ` ( a (,) b ) ) e. RR ) -> ( a e. RR /\ b e. RR ) )
21 20 ancoms 
 |-  ( ( ( vol* ` ( a (,) b ) ) e. RR /\ ( a (,) b ) =/= (/) ) -> ( a e. RR /\ b e. RR ) )
22 opelxpi 
 |-  ( ( a e. RR /\ b e. RR ) -> <. a , b >. e. ( RR X. RR ) )
23 21 22 syl 
 |-  ( ( ( vol* ` ( a (,) b ) ) e. RR /\ ( a (,) b ) =/= (/) ) -> <. a , b >. e. ( RR X. RR ) )
24 19 23 eqeltrd 
 |-  ( ( ( vol* ` ( a (,) b ) ) e. RR /\ ( a (,) b ) =/= (/) ) -> ( F ` ( a (,) b ) ) e. ( RR X. RR ) )
25 fveq2 
 |-  ( A = ( a (,) b ) -> ( vol* ` A ) = ( vol* ` ( a (,) b ) ) )
26 25 eleq1d 
 |-  ( A = ( a (,) b ) -> ( ( vol* ` A ) e. RR <-> ( vol* ` ( a (,) b ) ) e. RR ) )
27 neeq1 
 |-  ( A = ( a (,) b ) -> ( A =/= (/) <-> ( a (,) b ) =/= (/) ) )
28 26 27 anbi12d 
 |-  ( A = ( a (,) b ) -> ( ( ( vol* ` A ) e. RR /\ A =/= (/) ) <-> ( ( vol* ` ( a (,) b ) ) e. RR /\ ( a (,) b ) =/= (/) ) ) )
29 fveq2 
 |-  ( A = ( a (,) b ) -> ( F ` A ) = ( F ` ( a (,) b ) ) )
30 29 eleq1d 
 |-  ( A = ( a (,) b ) -> ( ( F ` A ) e. ( RR X. RR ) <-> ( F ` ( a (,) b ) ) e. ( RR X. RR ) ) )
31 28 30 imbi12d 
 |-  ( A = ( a (,) b ) -> ( ( ( ( vol* ` A ) e. RR /\ A =/= (/) ) -> ( F ` A ) e. ( RR X. RR ) ) <-> ( ( ( vol* ` ( a (,) b ) ) e. RR /\ ( a (,) b ) =/= (/) ) -> ( F ` ( a (,) b ) ) e. ( RR X. RR ) ) ) )
32 24 31 mpbiri 
 |-  ( A = ( a (,) b ) -> ( ( ( vol* ` A ) e. RR /\ A =/= (/) ) -> ( F ` A ) e. ( RR X. RR ) ) )
33 32 a1i 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( A = ( a (,) b ) -> ( ( ( vol* ` A ) e. RR /\ A =/= (/) ) -> ( F ` A ) e. ( RR X. RR ) ) ) )
34 33 rexlimivv 
 |-  ( E. a e. RR* E. b e. RR* A = ( a (,) b ) -> ( ( ( vol* ` A ) e. RR /\ A =/= (/) ) -> ( F ` A ) e. ( RR X. RR ) ) )
35 17 34 sylbi 
 |-  ( A e. ran (,) -> ( ( ( vol* ` A ) e. RR /\ A =/= (/) ) -> ( F ` A ) e. ( RR X. RR ) ) )
36 35 impl 
 |-  ( ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) /\ A =/= (/) ) -> ( F ` A ) e. ( RR X. RR ) )
37 13 36 pm2.61dane 
 |-  ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) -> ( F ` A ) e. ( RR X. RR ) )
38 5 37 elind 
 |-  ( ( A e. ran (,) /\ ( vol* ` A ) e. RR ) -> ( F ` A ) e. ( <_ i^i ( RR X. RR ) ) )