Definition df-oms 30354

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

Assertion

Ref	Expression
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 ) } |-> Σ* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < ) ) )

Distinct variable group:   r, a, x, y, z

Detailed syntax breakdown of Definition df-oms

Step	Hyp	Ref	Expression
1		coms 30353	. 2 class toOMeas
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		va	. . . 4 setvar a
5	2	cv 1482	. . . . . . 7 class r
6	5	cdm 5114	. . . . . 6 class dom r
7	6	cuni 4436	. . . . 5 class U. dom r
8	7	cpw 4158	. . . 4 class ~P U. dom r
9		vx	. . . . . . 7 setvar x
10	4	cv 1482	. . . . . . . . . 10 class a
11		vz	. . . . . . . . . . . 12 setvar z
12	11	cv 1482	. . . . . . . . . . 11 class z
13	12	cuni 4436	. . . . . . . . . 10 class U. z
14	10, 13	wss 3574	. . . . . . . . 9 wff a C_ U. z
15		com 7065	. . . . . . . . . 10 class om
16		cdom 7953	. . . . . . . . . 10 class ~<_
17	12, 15, 16	wbr 4653	. . . . . . . . 9 wff z ~<_ om
18	14, 17	wa 384	. . . . . . . 8 wff ( a C_ U. z /\ z ~<_ om )
19	6	cpw 4158	. . . . . . . 8 class ~P dom r
20	18, 11, 19	crab 2916	. . . . . . 7 class { z e. ~P dom r | ( a C_ U. z /\ z ~<_ om ) }
21	9	cv 1482	. . . . . . . 8 class x
22		vy	. . . . . . . . . 10 setvar y
23	22	cv 1482	. . . . . . . . 9 class y
24	23, 5	cfv 5888	. . . . . . . 8 class ( r ` y )
25	21, 24, 22	cesum 30089	. . . . . . 7 class Σ* y e. x ( r ` y )
26	9, 20, 25	cmpt 4729	. . . . . 6 class ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( r ` y ) )
27	26	crn 5115	. . . . 5 class ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( r ` y ) )
28		cc0 9936	. . . . . 6 class 0
29		cpnf 10071	. . . . . 6 class +oo
30		cicc 12178	. . . . . 6 class [,]
31	28, 29, 30	co 6650	. . . . 5 class ( 0 [,] +oo )
32		clt 10074	. . . . 5 class <
33	27, 31, 32	cinf 8347	. . . 4 class inf ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < )
34	4, 8, 33	cmpt 4729	. . 3 class ( a e. ~P U. dom r |-> inf ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < ) )
35	2, 3, 34	cmpt 4729	. 2 class ( r e. _V |-> ( a e. ~P U. dom r |-> inf ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < ) ) )
36	1, 35	wceq 1483	1 wff 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 ) } |-> Σ* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < ) ) )

This definition is referenced by:  omsval  30355