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