Metamath Proof Explorer

Theorem ovolval4lem2

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 , but here f is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval4lem2.a 
|- ( ph -> A C_ RR )
ovolval4lem2.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 ) ) ) }
ovolval4lem2.g 
|- G = ( n e. NN |-> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. )
Assertion ovolval4lem2 
|- ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ovolval4lem2.a 
 |-  ( ph -> A C_ RR )
2 ovolval4lem2.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 ) ) ) }
3 ovolval4lem2.g 
 |-  G = ( n e. NN |-> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. )
4 iftrue 
 |-  ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) -> if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) = ( 2nd ` ( f ` n ) ) )
5 4 opeq2d 
 |-  ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. = <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. )
6 5 adantl 
 |-  ( ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) /\ ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. = <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. )
7 df-br 
 |-  ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) <-> <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. e. <_ )
8 7 bilani 
 |-  ( ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) /\ ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) -> <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. e. <_ )
9 6 8 eqeltrd 
 |-  ( ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) /\ ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. e. <_ )
10 iffalse 
 |-  ( -. ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) -> if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) = ( 1st ` ( f ` n ) ) )
11 10 opeq2d 
 |-  ( -. ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. = <. ( 1st ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) >. )
12 11 adantl 
 |-  ( ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) /\ -. ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. = <. ( 1st ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) >. )
13 elmapi 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> f : NN --> ( RR X. RR ) )
14 13 ffvelcdmda 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( f ` n ) e. ( RR X. RR ) )
15 xp1st 
 |-  ( ( f ` n ) e. ( RR X. RR ) -> ( 1st ` ( f ` n ) ) e. RR )
16 14 15 syl 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( 1st ` ( f ` n ) ) e. RR )
17 16 leidd 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( 1st ` ( f ` n ) ) <_ ( 1st ` ( f ` n ) ) )
18 df-br 
 |-  ( ( 1st ` ( f ` n ) ) <_ ( 1st ` ( f ` n ) ) <-> <. ( 1st ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) >. e. <_ )
19 17 18 sylib 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> <. ( 1st ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) >. e. <_ )
20 19 adantr 
 |-  ( ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) /\ -. ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) -> <. ( 1st ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) >. e. <_ )
21 12 20 eqeltrd 
 |-  ( ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) /\ -. ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. e. <_ )
22 9 21 pm2.61dan 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. e. <_ )
23 xp2nd 
 |-  ( ( f ` n ) e. ( RR X. RR ) -> ( 2nd ` ( f ` n ) ) e. RR )
24 14 23 syl 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> ( 2nd ` ( f ` n ) ) e. RR )
25 24 16 ifcld 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) e. RR )
26 opelxpi 
 |-  ( ( ( 1st ` ( f ` n ) ) e. RR /\ if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) e. RR ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. e. ( RR X. RR ) )
27 16 25 26 syl2anc 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. e. ( RR X. RR ) )
28 22 27 elind 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ n e. NN ) -> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. e. ( <_ i^i ( RR X. RR ) ) )
29 28 3 fmptd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
30 reex 
 |-  RR e. _V
31 30 30 xpex 
 |-  ( RR X. RR ) e. _V
32 31 inex2 
 |-  ( <_ i^i ( RR X. RR ) ) e. _V
33 32 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( <_ i^i ( RR X. RR ) ) e. _V )
34 nnex 
 |-  NN e. _V
35 34 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> NN e. _V )
36 33 35 elmapd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> G : NN --> ( <_ i^i ( RR X. RR ) ) ) )
37 29 36 mpbird 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
38 37 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) -> G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
39 simpr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> A C_ U. ran ( (,) o. f ) )
40 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
41 40 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( RR X. RR ) C_ ( RR* X. RR* ) )
42 13 41 fssd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> f : NN --> ( RR* X. RR* ) )
43 2fveq3 
 |-  ( k = n -> ( 1st ` ( f ` k ) ) = ( 1st ` ( f ` n ) ) )
44 2fveq3 
 |-  ( k = n -> ( 2nd ` ( f ` k ) ) = ( 2nd ` ( f ` n ) ) )
45 43 44 breq12d 
 |-  ( k = n -> ( ( 1st ` ( f ` k ) ) <_ ( 2nd ` ( f ` k ) ) <-> ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) )
46 45 cbvrabv 
 |-  { k e. NN | ( 1st ` ( f ` k ) ) <_ ( 2nd ` ( f ` k ) ) } = { n e. NN | ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) }
47 42 3 46 ovolval4lem1 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( U. ran ( (,) o. f ) = U. ran ( (,) o. G ) /\ ( vol o. ( (,) o. f ) ) = ( vol o. ( (,) o. G ) ) ) )
48 47 simpld 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> U. ran ( (,) o. f ) = U. ran ( (,) o. G ) )
49 48 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> U. ran ( (,) o. f ) = U. ran ( (,) o. G ) )
50 39 49 sseqtrd 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ A C_ U. ran ( (,) o. f ) ) -> A C_ U. ran ( (,) o. G ) )
51 50 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. G ) )
52 simpr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) )
53 47 simprd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( vol o. ( (,) o. f ) ) = ( vol o. ( (,) o. G ) ) )
54 coass 
 |-  ( ( vol o. (,) ) o. f ) = ( vol o. ( (,) o. f ) )
55 54 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( ( vol o. (,) ) o. f ) = ( vol o. ( (,) o. f ) ) )
56 coass 
 |-  ( ( vol o. (,) ) o. G ) = ( vol o. ( (,) o. G ) )
57 56 a1i 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( ( vol o. (,) ) o. G ) = ( vol o. ( (,) o. G ) ) )
58 53 55 57 3eqtr4d 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( ( vol o. (,) ) o. f ) = ( ( vol o. (,) ) o. G ) )
59 58 fveq2d 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( vol o. (,) ) o. G ) ) )
60 59 adantr 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( vol o. (,) ) o. G ) ) )
61 52 60 eqtrd 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> y = ( sum^ ` ( ( vol o. (,) ) o. G ) ) )
62 61 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. G ) ) )
63 51 62 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. G ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. G ) ) ) )
64 coeq2 
 |-  ( g = G -> ( (,) o. g ) = ( (,) o. G ) )
65 64 rneqd 
 |-  ( g = G -> ran ( (,) o. g ) = ran ( (,) o. G ) )
66 65 unieqd 
 |-  ( g = G -> U. ran ( (,) o. g ) = U. ran ( (,) o. G ) )
67 66 sseq2d 
 |-  ( g = G -> ( A C_ U. ran ( (,) o. g ) <-> A C_ U. ran ( (,) o. G ) ) )
68 coeq2 
 |-  ( g = G -> ( ( vol o. (,) ) o. g ) = ( ( vol o. (,) ) o. G ) )
69 68 fveq2d 
 |-  ( g = G -> ( sum^ ` ( ( vol o. (,) ) o. g ) ) = ( sum^ ` ( ( vol o. (,) ) o. G ) ) )
70 69 eqeq2d 
 |-  ( g = G -> ( y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) <-> y = ( sum^ ` ( ( vol o. (,) ) o. G ) ) ) )
71 67 70 anbi12d 
 |-  ( g = G -> ( ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> ( A C_ U. ran ( (,) o. G ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. G ) ) ) ) )
72 71 rspcev 
 |-  ( ( G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. G ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. G ) ) ) ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) )
73 38 63 72 syl2anc 
 |-  ( ( f e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) )
74 73 rexlimiva 
 |-  ( E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) )
75 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
76 mapss 
 |-  ( ( ( RR X. RR ) e. _V /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) ) -> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) C_ ( ( RR X. RR ) ^m NN ) )
77 31 75 76 mp2an 
 |-  ( ( <_ i^i ( RR X. RR ) ) ^m NN ) C_ ( ( RR X. RR ) ^m NN )
78 77 sseli 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> g e. ( ( RR X. RR ) ^m NN ) )
79 78 adantr 
 |-  ( ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) ) -> g e. ( ( RR X. RR ) ^m NN ) )
80 simpr 
 |-  ( ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) ) -> ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) )
81 coeq2 
 |-  ( f = g -> ( (,) o. f ) = ( (,) o. g ) )
82 81 rneqd 
 |-  ( f = g -> ran ( (,) o. f ) = ran ( (,) o. g ) )
83 82 unieqd 
 |-  ( f = g -> U. ran ( (,) o. f ) = U. ran ( (,) o. g ) )
84 83 sseq2d 
 |-  ( f = g -> ( A C_ U. ran ( (,) o. f ) <-> A C_ U. ran ( (,) o. g ) ) )
85 coeq2 
 |-  ( f = g -> ( ( vol o. (,) ) o. f ) = ( ( vol o. (,) ) o. g ) )
86 85 fveq2d 
 |-  ( f = g -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( vol o. (,) ) o. g ) ) )
87 86 eqeq2d 
 |-  ( f = g -> ( y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) <-> y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) )
88 84 87 anbi12d 
 |-  ( f = g -> ( ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) ) )
89 88 rspcev 
 |-  ( ( g e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
90 79 80 89 syl2anc 
 |-  ( ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
91 90 rexlimiva 
 |-  ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
92 74 91 impbii 
 |-  ( E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) )
93 92 rabbii 
 |-  { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) } = { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) }
94 2 93 eqtri 
 |-  M = { y e. RR* | E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) }
95 1 94 ovolval3 
 |-  ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )