Definition df-mea

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

	Ref	Expression
Assertion	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 ) = ( sum^ ` ( x |` y ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmea	|- Meas
1		vx	|- x
2	1	cv	|- x
3	2	cdm	|- dom x
4		cc0	|- 0
5		cicc	|- [,]
6		cpnf	|- +oo
7	4 6 5	co	|- ( 0 [,] +oo )
8	3 7 2	wf	|- x : dom x --> ( 0 [,] +oo )
9		csalg	|- SAlg
10	3 9	wcel	|- dom x e. SAlg
11	8 10	wa	|- ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg )
12		c0	|- (/)
13	12 2	cfv	|- ( x ` (/) )
14	13 4	wceq	|- ( x ` (/) ) = 0
15	11 14	wa	|- ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg ) /\ ( x ` (/) ) = 0 )
16		vy	|- y
17	3	cpw	|- ~P dom x
18	16	cv	|- y
19		cdom	|- ~<_
20		com	|- _om
21	18 20 19	wbr	|- y ~<_ _om
22		vw	|- w
23	22	cv	|- w
24	22 18 23	wdisj	|- Disj_ w e. y w
25	21 24	wa	|- ( y ~<_ _om /\ Disj_ w e. y w )
26	18	cuni	|- U. y
27	26 2	cfv	|- ( x ` U. y )
28		csumge0	|- sum^
29	2 18	cres	|- ( x |` y )
30	29 28	cfv	|- ( sum^ ` ( x |` y ) )
31	27 30	wceq	|- ( x ` U. y ) = ( sum^ ` ( x |` y ) )
32	25 31	wi	|- ( ( y ~<_ _om /\ Disj_ w e. y w ) -> ( x ` U. y ) = ( sum^ ` ( x |` y ) ) )
33	32 16 17	wral	|- A. y e. ~P dom x ( ( y ~<_ _om /\ Disj_ w e. y w ) -> ( x ` U. y ) = ( sum^ ` ( x |` y ) ) )
34	15 33	wa	|- ( ( ( 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 ) = ( sum^ ` ( x |` y ) ) ) )
35	34 1	cab	|- { 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 ) = ( sum^ ` ( x |` y ) ) ) ) }
36	0 35	wceq	|- 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 ) = ( sum^ ` ( x |` y ) ) ) ) }