Metamath Proof Explorer

Theorem ovolval

Description: The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 17-Sep-2020)

Ref Expression
Hypothesis ovolval.1 
|- M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
Assertion ovolval 
|- ( A C_ RR -> ( vol* ` A ) = inf ( M , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ovolval.1 
 |-  M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
2 reex 
 |-  RR e. _V
3 2 elpw2 
 |-  ( A e. ~P RR <-> A C_ RR )
4 cleq1lem 
 |-  ( x = A -> ( ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
5 4 rexbidv 
 |-  ( x = A -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
6 5 rabbidv 
 |-  ( x = A -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } )
7 6 1 eqtr4di 
 |-  ( x = A -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = M )
8 7 infeq1d 
 |-  ( x = A -> inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) = inf ( M , RR* , < ) )
9 df-ovol 
 |-  vol* = ( x e. ~P RR |-> inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
10 xrltso 
 |-  < Or RR*
11 10 infex 
 |-  inf ( M , RR* , < ) e. _V
12 8 9 11 fvmpt 
 |-  ( A e. ~P RR -> ( vol* ` A ) = inf ( M , RR* , < ) )
13 3 12 sylbir 
 |-  ( A C_ RR -> ( vol* ` A ) = inf ( M , RR* , < ) )