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* , < ) ) |