Metamath Proof Explorer

Theorem omsval

Description: Value of the function mapping a content function to the corresponding outer measure. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion omsval 
|- ( R e. _V -> ( toOMeas ` R ) = ( a e. ~P U. dom R |-> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) ) )

Proof

Step Hyp Ref Expression
1 df-oms 
 |-  toOMeas = ( r e. _V |-> ( a e. ~P U. dom r |-> inf ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < ) ) )
2 dmeq 
 |-  ( r = R -> dom r = dom R )
3 2 unieqd 
 |-  ( r = R -> U. dom r = U. dom R )
4 3 pweqd 
 |-  ( r = R -> ~P U. dom r = ~P U. dom R )
5 2 pweqd 
 |-  ( r = R -> ~P dom r = ~P dom R )
6 rabeq 
 |-  ( ~P dom r = ~P dom R -> { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } = { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } )
7 5 6 syl 
 |-  ( r = R -> { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } = { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } )
8 simpl 
 |-  ( ( r = R /\ y e. x ) -> r = R )
9 8 fveq1d 
 |-  ( ( r = R /\ y e. x ) -> ( r ` y ) = ( R ` y ) )
10 9 esumeq2dv 
 |-  ( r = R -> sum* y e. x ( r ` y ) = sum* y e. x ( R ` y ) )
11 7 10 mpteq12dv 
 |-  ( r = R -> ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( r ` y ) ) = ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
12 11 rneqd 
 |-  ( r = R -> ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( r ` y ) ) = ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
13 12 infeq1d 
 |-  ( r = R -> inf ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < ) = inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
14 4 13 mpteq12dv 
 |-  ( r = R -> ( a e. ~P U. dom r |-> inf ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < ) ) = ( a e. ~P U. dom R |-> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) ) )
15 id 
 |-  ( R e. _V -> R e. _V )
16 dmexg 
 |-  ( R e. _V -> dom R e. _V )
17 uniexg 
 |-  ( dom R e. _V -> U. dom R e. _V )
18 pwexg 
 |-  ( U. dom R e. _V -> ~P U. dom R e. _V )
19 mptexg 
 |-  ( ~P U. dom R e. _V -> ( a e. ~P U. dom R |-> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) ) e. _V )
20 16 17 18 19 4syl 
 |-  ( R e. _V -> ( a e. ~P U. dom R |-> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) ) e. _V )
21 1 14 15 20 fvmptd3 
 |-  ( R e. _V -> ( toOMeas ` R ) = ( a e. ~P U. dom R |-> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) ) )