Metamath Proof Explorer

Theorem volicorescl

Description: The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion volicorescl 
|- ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( vol ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
2 1 reseq1i 
 |-  ( [,) |` ( RR X. RR ) ) = ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) )
3 ressxr 
 |-  RR C_ RR*
4 resmpo 
 |-  ( ( RR C_ RR* /\ RR C_ RR* ) -> ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) )
5 3 3 4 mp2an 
 |-  ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
6 2 5 eqtri 
 |-  ( [,) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
7 6 rneqi 
 |-  ran ( [,) |` ( RR X. RR ) ) = ran ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
8 7 eleq2i 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) <-> A e. ran ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) )
9 8 biimpi 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> A e. ran ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) )
10 eqid 
 |-  ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
11 xrex 
 |-  RR* e. _V
12 11 rabex 
 |-  { z e. RR* | ( x <_ z /\ z < y ) } e. _V
13 10 12 elrnmpo 
 |-  ( A e. ran ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) <-> E. x e. RR E. y e. RR A = { z e. RR* | ( x <_ z /\ z < y ) } )
14 9 13 sylib 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> E. x e. RR E. y e. RR A = { z e. RR* | ( x <_ z /\ z < y ) } )
15 simpr 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ A = { z e. RR* | ( x <_ z /\ z < y ) } ) -> A = { z e. RR* | ( x <_ z /\ z < y ) } )
16 3 sseli 
 |-  ( x e. RR -> x e. RR* )
17 16 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> x e. RR* )
18 3 sseli 
 |-  ( y e. RR -> y e. RR* )
19 18 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> y e. RR* )
20 icoval 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x [,) y ) = { z e. RR* | ( x <_ z /\ z < y ) } )
21 17 19 20 syl2anc 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x [,) y ) = { z e. RR* | ( x <_ z /\ z < y ) } )
22 21 eqcomd 
 |-  ( ( x e. RR /\ y e. RR ) -> { z e. RR* | ( x <_ z /\ z < y ) } = ( x [,) y ) )
23 22 adantr 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ A = { z e. RR* | ( x <_ z /\ z < y ) } ) -> { z e. RR* | ( x <_ z /\ z < y ) } = ( x [,) y ) )
24 15 23 eqtrd 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ A = { z e. RR* | ( x <_ z /\ z < y ) } ) -> A = ( x [,) y ) )
25 24 ex 
 |-  ( ( x e. RR /\ y e. RR ) -> ( A = { z e. RR* | ( x <_ z /\ z < y ) } -> A = ( x [,) y ) ) )
26 25 adantll 
 |-  ( ( ( A e. ran ( [,) |` ( RR X. RR ) ) /\ x e. RR ) /\ y e. RR ) -> ( A = { z e. RR* | ( x <_ z /\ z < y ) } -> A = ( x [,) y ) ) )
27 26 reximdva 
 |-  ( ( A e. ran ( [,) |` ( RR X. RR ) ) /\ x e. RR ) -> ( E. y e. RR A = { z e. RR* | ( x <_ z /\ z < y ) } -> E. y e. RR A = ( x [,) y ) ) )
28 27 reximdva 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( E. x e. RR E. y e. RR A = { z e. RR* | ( x <_ z /\ z < y ) } -> E. x e. RR E. y e. RR A = ( x [,) y ) ) )
29 14 28 mpd 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> E. x e. RR E. y e. RR A = ( x [,) y ) )
30 fveq2 
 |-  ( A = ( x [,) y ) -> ( vol ` A ) = ( vol ` ( x [,) y ) ) )
31 30 adantl 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ A = ( x [,) y ) ) -> ( vol ` A ) = ( vol ` ( x [,) y ) ) )
32 volicorecl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( vol ` ( x [,) y ) ) e. RR )
33 32 adantr 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ A = ( x [,) y ) ) -> ( vol ` ( x [,) y ) ) e. RR )
34 31 33 eqeltrd 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ A = ( x [,) y ) ) -> ( vol ` A ) e. RR )
35 34 ex 
 |-  ( ( x e. RR /\ y e. RR ) -> ( A = ( x [,) y ) -> ( vol ` A ) e. RR ) )
36 35 a1i 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( ( x e. RR /\ y e. RR ) -> ( A = ( x [,) y ) -> ( vol ` A ) e. RR ) ) )
37 36 rexlimdvv 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( E. x e. RR E. y e. RR A = ( x [,) y ) -> ( vol ` A ) e. RR ) )
38 29 37 mpd 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( vol ` A ) e. RR )
39 38 2a1d 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( ( x e. RR /\ y e. RR ) -> ( A = ( x [,) y ) -> ( vol ` A ) e. RR ) ) )
40 39 rexlimdvv 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( E. x e. RR E. y e. RR A = ( x [,) y ) -> ( vol ` A ) e. RR ) )
41 29 40 mpd 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( vol ` A ) e. RR )