Definition df-mea 40667

Description: Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
df-mea	|- Meas = { x | ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P dom x ( ( y ~<_ om /\ Disj w e. y w ) -> ( x ` U. y ) = (Σ^ ` ( x |` y ) ) ) ) }

Distinct variable group:   x, w, y

Detailed syntax breakdown of Definition df-mea

Step	Hyp	Ref	Expression
1		cmea 40666	. 2 class Meas
2		vx	. . . . . . . . 9 setvar x
3	2	cv 1482	. . . . . . . 8 class x
4	3	cdm 5114	. . . . . . 7 class dom x
5		cc0 9936	. . . . . . . 8 class 0
6		cpnf 10071	. . . . . . . 8 class +oo
7		cicc 12178	. . . . . . . 8 class [,]
8	5, 6, 7	co 6650	. . . . . . 7 class ( 0 [,] +oo )
9	4, 8, 3	wf 5884	. . . . . 6 wff x : dom x --> ( 0 [,] +oo )
10		csalg 40528	. . . . . . 7 class SAlg
11	4, 10	wcel 1990	. . . . . 6 wff dom x e. SAlg
12	9, 11	wa 384	. . . . 5 wff ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg )
13		c0 3915	. . . . . . 7 class (/)
14	13, 3	cfv 5888	. . . . . 6 class ( x ` (/) )
15	14, 5	wceq 1483	. . . . 5 wff ( x ` (/) ) = 0
16	12, 15	wa 384	. . . 4 wff ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg ) /\ ( x ` (/) ) = 0 )
17		vy	. . . . . . . . 9 setvar y
18	17	cv 1482	. . . . . . . 8 class y
19		com 7065	. . . . . . . 8 class om
20		cdom 7953	. . . . . . . 8 class ~<_
21	18, 19, 20	wbr 4653	. . . . . . 7 wff y ~<_ om
22		vw	. . . . . . . 8 setvar w
23	22	cv 1482	. . . . . . . 8 class w
24	22, 18, 23	wdisj 4620	. . . . . . 7 wff Disj w e. y w
25	21, 24	wa 384	. . . . . 6 wff ( y ~<_ om /\ Disj w e. y w )
26	18	cuni 4436	. . . . . . . 8 class U. y
27	26, 3	cfv 5888	. . . . . . 7 class ( x ` U. y )
28	3, 18	cres 5116	. . . . . . . 8 class ( x |` y )
29		csumge0 40579	. . . . . . . 8 class Σ^
30	28, 29	cfv 5888	. . . . . . 7 class (Σ^ ` ( x |` y ) )
31	27, 30	wceq 1483	. . . . . 6 wff ( x ` U. y ) = (Σ^ ` ( x |` y ) )
32	25, 31	wi 4	. . . . 5 wff ( ( y ~<_ om /\ Disj w e. y w ) -> ( x ` U. y ) = (Σ^ ` ( x |` y ) ) )
33	4	cpw 4158	. . . . 5 class ~P dom x
34	32, 17, 33	wral 2912	. . . 4 wff A. y e. ~P dom x ( ( y ~<_ om /\ Disj w e. y w ) -> ( x ` U. y ) = (Σ^ ` ( x |` y ) ) )
35	16, 34	wa 384	. . 3 wff ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P dom x ( ( y ~<_ om /\ Disj w e. y w ) -> ( x ` U. y ) = (Σ^ ` ( x |` y ) ) ) )
36	35, 2	cab 2608	. 2 class { x | ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P dom x ( ( y ~<_ om /\ Disj w e. y w ) -> ( x ` U. y ) = (Σ^ ` ( x |` y ) ) ) ) }
37	1, 36	wceq 1483	1 wff Meas = { x | ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P dom x ( ( y ~<_ om /\ Disj w e. y w ) -> ( x ` U. y ) = (Σ^ ` ( x |` y ) ) ) ) }

This definition is referenced by:  ismea  40668