Metamath Proof Explorer

Theorem ovolval5

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 ovolval5.a 
|- ( ph -> A C_ RR )
ovolval5.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 ) ) ) }
Assertion ovolval5 
|- ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ovolval5.a 
 |-  ( ph -> A C_ RR )
2 ovolval5.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 eqeq1 
 |-  ( x = y -> ( x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) <-> y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) )
4 3 anbi2d 
 |-  ( x = y -> ( ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) ) )
5 4 rexbidv 
 |-  ( x = y -> ( E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) ) )
6 coeq2 
 |-  ( g = f -> ( (,) o. g ) = ( (,) o. f ) )
7 6 rneqd 
 |-  ( g = f -> ran ( (,) o. g ) = ran ( (,) o. f ) )
8 7 unieqd 
 |-  ( g = f -> U. ran ( (,) o. g ) = U. ran ( (,) o. f ) )
9 8 sseq2d 
 |-  ( g = f -> ( A C_ U. ran ( (,) o. g ) <-> A C_ U. ran ( (,) o. f ) ) )
10 coeq2 
 |-  ( g = f -> ( ( vol o. (,) ) o. g ) = ( ( vol o. (,) ) o. f ) )
11 10 fveq2d 
 |-  ( g = f -> ( sum^ ` ( ( vol o. (,) ) o. g ) ) = ( sum^ ` ( ( vol o. (,) ) o. f ) ) )
12 11 eqeq2d 
 |-  ( g = f -> ( y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) <-> y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
13 9 12 anbi12d 
 |-  ( g = f -> ( ( A C_ U. ran ( (,) o. g ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
14 13 cbvrexvw 
 |-  ( E. 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 ) ) ) )
15 14 a1i 
 |-  ( x = y -> ( E. 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 ) ) ) ) )
16 5 15 bitrd 
 |-  ( x = y -> ( E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( 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 ) ) ) ) )
17 16 cbvrabv 
 |-  { x e. RR* | E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) } = { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
18 1 17 ovolval4 
 |-  ( ph -> ( vol* ` A ) = inf ( { x e. RR* | E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) } , RR* , < ) )
19 11 eqeq2d 
 |-  ( g = f -> ( x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) <-> x = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
20 9 19 anbi12d 
 |-  ( g = f -> ( ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
21 20 cbvrexvw 
 |-  ( E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
22 21 a1i 
 |-  ( x = z -> ( E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) <-> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
23 eqeq1 
 |-  ( x = z -> ( x = ( sum^ ` ( ( vol o. (,) ) o. f ) ) <-> z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
24 23 anbi2d 
 |-  ( x = z -> ( ( A C_ U. ran ( (,) o. f ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
25 24 rexbidv 
 |-  ( x = z -> ( E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
26 22 25 bitrd 
 |-  ( x = z -> ( E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( 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 cbvrabv 
 |-  { x e. RR* | E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( 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 ovolval5lem3 
 |-  inf ( { x e. RR* | E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) } , RR* , < ) = inf ( M , RR* , < )
29 28 a1i 
 |-  ( ph -> inf ( { x e. RR* | E. g e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. g ) /\ x = ( sum^ ` ( ( vol o. (,) ) o. g ) ) ) } , RR* , < ) = inf ( M , RR* , < ) )
30 18 29 eqtrd 
 |-  ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )