Metamath Proof Explorer

Definition df-oms

Description: Define a function constructing an outer measure. See omsval for its value. Definition 1.5 of Bogachev p. 16. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion 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 ) , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 coms 
 |-  toOMeas
1 vr 
 |-  r
2 cvv 
 |-  _V
3 va 
 |-  a
4 1 cv 
 |-  r
5 4 cdm 
 |-  dom r
6 5 cuni 
 |-  U. dom r
7 6 cpw 
 |-  ~P U. dom r
8 vx 
 |-  x
9 vz 
 |-  z
10 5 cpw 
 |-  ~P dom r
11 3 cv 
 |-  a
12 9 cv 
 |-  z
13 12 cuni 
 |-  U. z
14 11 13 wss 
 |-  a C_ U. z
15 cdom 
 |-  ~<_
16 com 
 |-  _om
17 12 16 15 wbr 
 |-  z ~<_ _om
18 14 17 wa 
 |-  ( a C_ U. z /\ z ~<_ _om )
19 18 9 10 crab 
 |-  { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) }
20 vy 
 |-  y
21 8 cv 
 |-  x
22 20 cv 
 |-  y
23 22 4 cfv 
 |-  ( r ` y )
24 21 23 20 cesum 
 |-  sum* y e. x ( r ` y )
25 8 19 24 cmpt 
 |-  ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( r ` y ) )
26 25 crn 
 |-  ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( r ` y ) )
27 cc0 
 |-  0
28 cicc 
 |-  [,]
29 cpnf 
 |-  +oo
30 27 29 28 co 
 |-  ( 0 [,] +oo )
31 clt 
 |-  <
32 26 30 31 cinf 
 |-  inf ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < )
33 3 7 32 cmpt 
 |-  ( 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 ) , < ) )
34 1 2 33 cmpt 
 |-  ( 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 ) , < ) ) )
35 0 34 wceq 
 |-  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 ) , < ) ) )