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 ssrab2 
 |-  { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) } C_ RR*
4 2 3 eqsstri 
 |-  Q C_ RR*
5 infxrcl 
 |-  ( Q C_ RR* -> inf ( Q , RR* , < ) e. RR* )
6 4 5 mp1i 
 |-  ( T. -> inf ( Q , RR* , < ) e. RR* )
7 ssrab2 
 |-  { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) } C_ RR*
8 1 7 eqsstri 
 |-  M C_ RR*
9 infxrcl 
 |-  ( M C_ RR* -> inf ( M , RR* , < ) e. RR* )
10 8 9 mp1i 
 |-  ( T. -> inf ( M , RR* , < ) e. RR* )
11 4 a1i 
 |-  ( T. -> Q C_ RR* )
12 8 a1i 
 |-  ( T. -> M C_ RR* )
13 simpr 
 |-  ( ( y e. M /\ w e. RR+ ) -> w e. RR+ )
14 1 rabeq2i 
 |-  ( 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 ) ) ) ) )
15 14 biimpi 
 |-  ( 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 ) ) ) ) )
16 15 simprd 
 |-  ( y e. M -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )
17 16 adantr 
 |-  ( ( y e. M /\ w e. RR+ ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( [,) o. f ) /\ y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )
18 coeq2 
 |-  ( g = f -> ( (,) o. g ) = ( (,) o. f ) )
19 18 rneqd 
 |-  ( g = f -> ran ( (,) o. g ) = ran ( (,) o. f ) )
20 19 unieqd 
 |-  ( g = f -> U. ran ( (,) o. g ) = U. ran ( (,) o. f ) )
21 20 sseq2d 
 |-  ( g = f -> ( A C_ U. ran ( (,) o. g ) <-> A C_ U. ran ( (,) o. f ) ) )
22 coeq2 
 |-  ( g = f -> ( ( vol o. (,) ) o. g ) = ( ( vol o. (,) ) o. f ) )
23 22 fveq2d 
 |-  ( g = f -> ( sum^ ` ( ( vol o. (,) ) o. g ) ) = ( sum^ ` ( ( vol o. (,) ) o. f ) ) )
24 23 eqeq2d 
 |-  ( g = f -> ( z = ( sum^ ` ( ( vol o. (,) ) o. g ) ) <-> z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
25 21 24 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 ) ) ) ) )
26 25 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 ) ) ) )
27 26 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 ) ) ) }
28 2 27 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 ) ) ) }
29 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 ) ) )
30 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 ) ) >. ) ) )
31 elmapi 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> f : NN --> ( RR X. RR ) )
32 31 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 ) )
33 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 ) )
34 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+ )
35 2fveq3 
 |-  ( m = n -> ( 1st ` ( f ` m ) ) = ( 1st ` ( f ` n ) ) )
36 oveq2 
 |-  ( m = n -> ( 2 ^ m ) = ( 2 ^ n ) )
37 36 oveq2d 
 |-  ( m = n -> ( w / ( 2 ^ m ) ) = ( w / ( 2 ^ n ) ) )
38 35 37 oveq12d 
 |-  ( m = n -> ( ( 1st ` ( f ` m ) ) - ( w / ( 2 ^ m ) ) ) = ( ( 1st ` ( f ` n ) ) - ( w / ( 2 ^ n ) ) ) )
39 2fveq3 
 |-  ( m = n -> ( 2nd ` ( f ` m ) ) = ( 2nd ` ( f ` n ) ) )
40 38 39 opeq12d 
 |-  ( m = n -> <. ( ( 1st ` ( f ` m ) ) - ( w / ( 2 ^ m ) ) ) , ( 2nd ` ( f ` m ) ) >. = <. ( ( 1st ` ( f ` n ) ) - ( w / ( 2 ^ n ) ) ) , ( 2nd ` ( f ` n ) ) >. )
41 40 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 ) ) >. )
42 28 29 30 32 33 34 41 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 ) )
43 42 3exp 
 |-  ( 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 ) ) ) )
44 43 rexlimdv 
 |-  ( 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 ) ) )
45 44 imp 
 |-  ( ( 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 ) )
46 13 17 45 syl2anc 
 |-  ( ( y e. M /\ w e. RR+ ) -> E. z e. Q z <_ ( y +e w ) )
47 46 3adant1 
 |-  ( ( T. /\ y e. M /\ w e. RR+ ) -> E. z e. Q z <_ ( y +e w ) )
48 11 12 47 infleinf 
 |-  ( T. -> inf ( Q , RR* , < ) <_ inf ( M , RR* , < ) )
49 eqeq1 
 |-  ( z = y -> ( z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) <-> y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
50 49 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 ) ) ) ) )
51 50 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 ) ) ) ) )
52 51 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 ) ) ) }
53 simpr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> A C_ U. ran ( (,) o. f ) )
54 ioossico 
 |-  ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) C_ ( ( 1st ` ( f ` n ) ) [,) ( 2nd ` ( f ` n ) ) )
55 54 a1i 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) C_ ( ( 1st ` ( f ` n ) ) [,) ( 2nd ` ( f ` n ) ) ) )
56 31 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> f : NN --> ( RR X. RR ) )
57 simpr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> n e. NN )
58 56 57 fvovco 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( (,) o. f ) ` n ) = ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) )
59 56 57 fvovco 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( [,) o. f ) ` n ) = ( ( 1st ` ( f ` n ) ) [,) ( 2nd ` ( f ` n ) ) ) )
60 58 59 sseq12d 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( ( (,) o. f ) ` n ) C_ ( ( [,) o. f ) ` n ) <-> ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) C_ ( ( 1st ` ( f ` n ) ) [,) ( 2nd ` ( f ` n ) ) ) ) )
61 55 60 mpbird 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( ( (,) o. f ) ` n ) C_ ( ( [,) o. f ) ` n ) )
62 61 ralrimiva 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> A. n e. NN ( ( (,) o. f ) ` n ) C_ ( ( [,) o. f ) ` n ) )
63 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 ) )
64 62 63 syl 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U_ n e. NN ( ( (,) o. f ) ` n ) C_ U_ n e. NN ( ( [,) o. f ) ` n ) )
65 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
66 65 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> (,) : ( RR* X. RR* ) --> ~P RR )
67 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
68 67 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( RR X. RR ) C_ ( RR* X. RR* ) )
69 31 68 fssd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> f : NN --> ( RR* X. RR* ) )
70 fco 
 |-  ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ f : NN --> ( RR* X. RR* ) ) -> ( (,) o. f ) : NN --> ~P RR )
71 66 69 70 syl2anc 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( (,) o. f ) : NN --> ~P RR )
72 71 ffnd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( (,) o. f ) Fn NN )
73 fniunfv 
 |-  ( ( (,) o. f ) Fn NN -> U_ n e. NN ( ( (,) o. f ) ` n ) = U. ran ( (,) o. f ) )
74 72 73 syl 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U_ n e. NN ( ( (,) o. f ) ` n ) = U. ran ( (,) o. f ) )
75 icof 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
76 75 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> [,) : ( RR* X. RR* ) --> ~P RR* )
77 fco 
 |-  ( ( [,) : ( RR* X. RR* ) --> ~P RR* /\ f : NN --> ( RR* X. RR* ) ) -> ( [,) o. f ) : NN --> ~P RR* )
78 76 69 77 syl2anc 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( [,) o. f ) : NN --> ~P RR* )
79 78 ffnd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( [,) o. f ) Fn NN )
80 fniunfv 
 |-  ( ( [,) o. f ) Fn NN -> U_ n e. NN ( ( [,) o. f ) ` n ) = U. ran ( [,) o. f ) )
81 79 80 syl 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U_ n e. NN ( ( [,) o. f ) ` n ) = U. ran ( [,) o. f ) )
82 74 81 sseq12d 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( U_ n e. NN ( ( (,) o. f ) ` n ) C_ U_ n e. NN ( ( [,) o. f ) ` n ) <-> U. ran ( (,) o. f ) C_ U. ran ( [,) o. f ) ) )
83 64 82 mpbid 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U. ran ( (,) o. f ) C_ U. ran ( [,) o. f ) )
84 83 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> U. ran ( (,) o. f ) C_ U. ran ( [,) o. f ) )
85 53 84 sstrd 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> A C_ U. ran ( [,) o. f ) )
86 85 adantrr 
 |-  ( ( 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 ) )
87 simpr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) )
88 31 voliooicof 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( ( vol o. (,) ) o. f ) = ( ( vol o. [,) ) o. f ) )
89 88 fveq2d 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( vol o. [,) ) o. f ) ) )
90 89 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( vol o. [,) ) o. f ) ) )
91 87 90 eqtrd 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> y = ( sum^ ` ( ( vol o. [,) ) o. f ) ) )
92 91 adantrl 
 |-  ( ( 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 ) ) )
93 86 92 jca 
 |-  ( ( 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 ) ) ) )
94 93 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 ) ) ) ) )
95 94 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 ) ) ) )
96 95 rgenw 
 |-  A. 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 ) ) ) )
97 ss2rab 
 |-  ( { 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 ) ) ) } <-> A. 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 ) ) ) ) )
98 96 97 mpbir 
 |-  { 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 ) ) ) }
99 52 98 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 ) ) ) }
100 2 1 sseq12i 
 |-  ( Q C_ M <-> { 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 ) ) ) } )
101 99 100 mpbir 
 |-  Q C_ M
102 infxrss 
 |-  ( ( Q C_ M /\ M C_ RR* ) -> inf ( M , RR* , < ) <_ inf ( Q , RR* , < ) )
103 101 8 102 mp2an 
 |-  inf ( M , RR* , < ) <_ inf ( Q , RR* , < )
104 103 a1i 
 |-  ( T. -> inf ( M , RR* , < ) <_ inf ( Q , RR* , < ) )
105 6 10 48 104 xrletrid 
 |-  ( T. -> inf ( Q , RR* , < ) = inf ( M , RR* , < ) )
106 105 mptru 
 |-  inf ( Q , RR* , < ) = inf ( M , RR* , < )