Definition df-meas 30259

Description: Define a measure as a nonnegative countably additive function over a sigma-algebra onto ( 0 [,] +oo ). (Contributed by Thierry Arnoux, 10-Sep-2016.)

Assertion

Ref	Expression
df-meas	|- measures = ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) ) ) } )

Distinct variable group:   x, m, y, s

Detailed syntax breakdown of Definition df-meas

Step	Hyp	Ref	Expression
1		cmeas 30258	. 2 class measures
2		vs	. . 3 setvar s
3		csiga 30170	. . . . 5 class sigAlgebra
4	3	crn 5115	. . . 4 class ran sigAlgebra
5	4	cuni 4436	. . 3 class U. ran sigAlgebra
6	2	cv 1482	. . . . . 6 class s
7		cc0 9936	. . . . . . 7 class 0
8		cpnf 10071	. . . . . . 7 class +oo
9		cicc 12178	. . . . . . 7 class [,]
10	7, 8, 9	co 6650	. . . . . 6 class ( 0 [,] +oo )
11		vm	. . . . . . 7 setvar m
12	11	cv 1482	. . . . . 6 class m
13	6, 10, 12	wf 5884	. . . . 5 wff m : s --> ( 0 [,] +oo )
14		c0 3915	. . . . . . 7 class (/)
15	14, 12	cfv 5888	. . . . . 6 class ( m ` (/) )
16	15, 7	wceq 1483	. . . . 5 wff ( m ` (/) ) = 0
17		vx	. . . . . . . . . 10 setvar x
18	17	cv 1482	. . . . . . . . 9 class x
19		com 7065	. . . . . . . . 9 class om
20		cdom 7953	. . . . . . . . 9 class ~<_
21	18, 19, 20	wbr 4653	. . . . . . . 8 wff x ~<_ om
22		vy	. . . . . . . . 9 setvar y
23	22	cv 1482	. . . . . . . . 9 class y
24	22, 18, 23	wdisj 4620	. . . . . . . 8 wff Disj y e. x y
25	21, 24	wa 384	. . . . . . 7 wff ( x ~<_ om /\ Disj y e. x y )
26	18	cuni 4436	. . . . . . . . 9 class U. x
27	26, 12	cfv 5888	. . . . . . . 8 class ( m ` U. x )
28	23, 12	cfv 5888	. . . . . . . . 9 class ( m ` y )
29	18, 28, 22	cesum 30089	. . . . . . . 8 class Σ* y e. x ( m ` y )
30	27, 29	wceq 1483	. . . . . . 7 wff ( m ` U. x ) = Σ* y e. x ( m ` y )
31	25, 30	wi 4	. . . . . 6 wff ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) )
32	6	cpw 4158	. . . . . 6 class ~P s
33	31, 17, 32	wral 2912	. . . . 5 wff A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) )
34	13, 16, 33	w3a 1037	. . . 4 wff ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) ) )
35	34, 11	cab 2608	. . 3 class { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) ) ) }
36	2, 5, 35	cmpt 4729	. 2 class ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) ) ) } )
37	1, 36	wceq 1483	1 wff measures = ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) ) ) } )

This definition is referenced by:  measbase  30260  measval  30261  ismeas  30262  isrnmeas  30263  measbasedom  30265