Metamath Proof Explorer

Theorem ovolval5lem3

Description: The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval5lem3.m 
|- M = { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) }
ovolval5lem3.q 
|- Q = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
Assertion ovolval5lem3 
|- inf ( Q , RR* , < ) = inf ( M , RR* , < )

Proof

Step Hyp Ref Expression
1 ovolval5lem3.m 
 |-  M = { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) }
2 ovolval5lem3.q 
 |-  Q = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
3 2 ssrab3 
 |-  Q C_ RR*
4 infxrcl 
 |-  ( Q C_ RR* -> inf ( Q , RR* , < ) e. RR* )
5 3 4 mp1i 
 |-  ( T. -> inf ( Q , RR* , < ) e. RR* )
6 1 ssrab3 
 |-  M C_ RR*
7 infxrcl 
 |-  ( M C_ RR* -> inf ( M , RR* , < ) e. RR* )
8 6 7 mp1i 
 |-  ( T. -> inf ( M , RR* , < ) e. RR* )
9 3 a1i 
 |-  ( T. -> Q C_ RR* )
10 6 a1i 
 |-  ( T. -> M C_ RR* )
11 1 reqabi 
 |-  ( y e. M <-> ( y e. RR* /\ E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) )
12 11 simprbi 
 |-  ( y e. M -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )
13 coeq2 
 |-  ( g = f -> ( (,) o. g ) = ( (,) o. f ) )
14 13 rneqd 
 |-  ( g = f -> ran ( (,) o. g ) = ran ( (,) o. f ) )
15 14 unieqd 
 |-  ( g = f -> U. ran ( (,) o. g ) = U. ran ( (,) o. f ) )
16 15 sseq2d 
 |-  ( g = f -> ( A C_ U. ran ( (,) o. g ) <-> A C_ U. ran ( (,) o. f ) ) )
17 coeq2 
 |-  ( g = f -> ( ( vol o. (,) ) o. g ) = ( ( vol o. (,) ) o. f ) )
18 17 fveq2d 
 |-  ( g = f -> ( sum^ ` ( ( vol o. (,) ) o. g ) ) = ( sum^ ` ( ( vol o. (,) ) o. f ) ) )
19 18 eqeq2d 
 |-  ( g = f -> ( z = ( sum^ ` ( ( vol o. (,) ) o. g ) ) <-> z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
20 16 19 anbi12d 
 |-  ( g = f -> ( ( A C_ U. ran ( (,) o. g ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
21 20 cbvrexvw 
 |-  ( E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
22 21 rabbii 
 |-  { z e. RR* | E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) } = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
23 2 22 eqtr4i 
 |-  Q = { z e. RR* | E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) }
24 simp3r 
 |-  ( ( w e. RR+ /\ f e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) )
25 eqid 
 |-  ( sum^ ` ( ( vol o. (,) ) o. ( m e. NN |-> <. ( ( 1st ` ( f ` m ) ) - ( w / ( 2 ^ m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) ) ) = ( sum^ ` ( ( vol o. (,) ) o. ( m e. NN |-> <. ( ( 1st ` ( f ` m ) ) - ( w / ( 2 ^ m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) ) )
26 elmapi 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> f : NN --> ( RR X. RR ) )
27 26 3ad2ant2 
 |-  ( ( w e. RR+ /\ f e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> f : NN --> ( RR X. RR ) )
28 simp3l 
 |-  ( ( w e. RR+ /\ f e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> A C_ U. ran ( [,) o. f ) )
29 simp1 
 |-  ( ( w e. RR+ /\ f e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> w e. RR+ )
30 2fveq3 
 |-  ( m = n -> ( 1st ` ( f ` m ) ) = ( 1st ` ( f ` n ) ) )
31 oveq2 
 |-  ( m = n -> ( 2 ^ m ) = ( 2 ^ n ) )
32 31 oveq2d 
 |-  ( m = n -> ( w / ( 2 ^ m ) ) = ( w / ( 2 ^ n ) ) )
33 30 32 oveq12d 
 |-  ( m = n -> ( ( 1st ` ( f ` m ) ) - ( w / ( 2 ^ m ) ) ) = ( ( 1st ` ( f ` n ) ) - ( w / ( 2 ^ n ) ) ) )
34 2fveq3 
 |-  ( m = n -> ( 2nd ` ( f ` m ) ) = ( 2nd ` ( f ` n ) ) )
35 33 34 opeq12d 
 |-  ( m = n -> <. ( ( 1st ` ( f ` m ) ) - ( w / ( 2 ^ m ) ) ) , ( 2nd ` ( f ` m ) ) >. = <. ( ( 1st ` ( f ` n ) ) - ( w / ( 2 ^ n ) ) ) , ( 2nd ` ( f ` n ) ) >. )
36 35 cbvmptv 
 |-  ( m e. NN |-> <. ( ( 1st ` ( f ` m ) ) - ( w / ( 2 ^ m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) = ( n e. NN |-> <. ( ( 1st ` ( f ` n ) ) - ( w / ( 2 ^ n ) ) ) , ( 2nd ` ( f ` n ) ) >. )
37 23 24 25 27 28 29 36 ovolval5lem2 
 |-  ( ( w e. RR+ /\ f e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) -> E. z e. Q z <_ ( y +e w ) )
38 37 rexlimdv3a 
 |-  ( w e. RR+ -> ( E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) -> E. z e. Q z <_ ( y +e w ) ) )
39 12 38 mpan9 
 |-  ( ( y e. M /\ w e. RR+ ) -> E. z e. Q z <_ ( y +e w ) )
40 39 3adant1 
 |-  ( ( T. /\ y e. M /\ w e. RR+ ) -> E. z e. Q z <_ ( y +e w ) )
41 9 10 40 infleinf 
 |-  ( T. -> inf ( Q , RR* , < ) <_ inf ( M , RR* , < ) )
42 eqeq1 
 |-  ( z = y -> ( z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) <-> y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
43 42 anbi2d 
 |-  ( z = y -> ( ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
44 43 rexbidv 
 |-  ( z = y -> ( E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
45 44 cbvrabv 
 |-  { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) } = { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
46 simpr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> A C_ U. ran ( (,) o. f ) )
47 ioossico 
 |-  ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) C_ ( ( 1st ` ( f ` n ) ) [,) ( 2nd ` ( f ` n ) ) )
48 47 a1i 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) C_ ( ( 1st ` ( f ` n ) ) [,) ( 2nd ` ( f ` n ) ) ) )
49 26 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> f : NN --> ( RR X. RR ) )
50 simpr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> n e. NN )
51 49 50 fvovco 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( (,) o. f ) ` n ) = ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) )
52 49 50 fvovco 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( [,) o. f ) ` n ) = ( ( 1st ` ( f ` n ) ) [,) ( 2nd ` ( f ` n ) ) ) )
53 48 51 52 3sstr4d 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( (,) o. f ) ` n ) C_ ( ( [,) o. f ) ` n ) )
54 53 ralrimiva 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> A. n e. NN ( ( (,) o. f ) ` n ) C_ ( ( [,) o. f ) ` n ) )
55 ss2iun 
 |-  ( A. n e. NN ( ( (,) o. f ) ` n ) C_ ( ( [,) o. f ) ` n ) -> U_ n e. NN ( ( (,) o. f ) ` n ) C_ U_ n e. NN ( ( [,) o. f ) ` n ) )
56 54 55 syl 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U_ n e. NN ( ( (,) o. f ) ` n ) C_ U_ n e. NN ( ( [,) o. f ) ` n ) )
57 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
58 57 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> (,) : ( RR* X. RR* ) --> ~P RR )
59 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
60 59 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( RR X. RR ) C_ ( RR* X. RR* ) )
61 58 60 26 fcoss 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( (,) o. f ) : NN --> ~P RR )
62 61 ffnd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( (,) o. f ) Fn NN )
63 fniunfv 
 |-  ( ( (,) o. f ) Fn NN -> U_ n e. NN ( ( (,) o. f ) ` n ) = U. ran ( (,) o. f ) )
64 62 63 syl 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U_ n e. NN ( ( (,) o. f ) ` n ) = U. ran ( (,) o. f ) )
65 icof 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
66 65 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> [,) : ( RR* X. RR* ) --> ~P RR* )
67 66 60 26 fcoss 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( [,) o. f ) : NN --> ~P RR* )
68 67 ffnd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( [,) o. f ) Fn NN )
69 fniunfv 
 |-  ( ( [,) o. f ) Fn NN -> U_ n e. NN ( ( [,) o. f ) ` n ) = U. ran ( [,) o. f ) )
70 68 69 syl 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U_ n e. NN ( ( [,) o. f ) ` n ) = U. ran ( [,) o. f ) )
71 56 64 70 3sstr3d 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U. ran ( (,) o. f ) C_ U. ran ( [,) o. f ) )
72 71 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> U. ran ( (,) o. f ) C_ U. ran ( [,) o. f ) )
73 46 72 sstrd 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> A C_ U. ran ( [,) o. f ) )
74 simpr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) )
75 26 voliooicof 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( ( vol o. (,) ) o. f ) = ( ( vol o. [,) ) o. f ) )
76 75 fveq2d 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( vol o. [,) ) o. f ) ) )
77 76 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( vol o. [,) ) o. f ) ) )
78 74 77 eqtrd 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) )
79 73 78 anim12dan 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) -> ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )
80 79 ex 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) )
81 80 reximia 
 |-  ( E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )
82 81 a1i 
 |-  ( y e. RR* -> ( E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) )
83 82 ss2rabi 
 |-  { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) } C_ { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) }
84 45 83 eqsstri 
 |-  { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) } C_ { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) }
85 84 2 1 3sstr4i 
 |-  Q C_ M
86 infxrss 
 |-  ( ( Q C_ M /\ M C_ RR* ) -> inf ( M , RR* , < ) <_ inf ( Q , RR* , < ) )
87 85 6 86 mp2an 
 |-  inf ( M , RR* , < ) <_ inf ( Q , RR* , < )
88 87 a1i 
 |-  ( T. -> inf ( M , RR* , < ) <_ inf ( Q , RR* , < ) )
89 5 8 41 88 xrletrid 
 |-  ( T. -> inf ( Q , RR* , < ) = inf ( M , RR* , < ) )
90 89 mptru 
 |-  inf ( Q , RR* , < ) = inf ( M , RR* , < )