Definition df-meas

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

	Ref	Expression
Assertion	df-meas	$$⊢\mathrm{measures}=\left(s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}⟼\left\{m|\left(m:s⟶\left[0,\mathrm{+\infty }\right]\wedge m\left(\varnothing \right)=0\wedge \forall x\in 𝒫s\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to m\left(\bigcup x\right)=\underset{y\in x}{{\sum }^{*}}m\left(y\right)\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmeas	$$class\mathrm{measures}$$
1		vs	$$setvars$$
2		csiga	$$class\mathrm{sigAlgebra}$$
3	2	crn	$$class\mathrm{ran}\mathrm{sigAlgebra}$$
4	3	cuni	$$class\bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
5		vm	$$setvarm$$
6	5	cv	$$setvarm$$
7	1	cv	$$setvars$$
8		cc0	$$class0$$
9		cicc	$$class\left[.\right]$$
10		cpnf	$$class\mathrm{+\infty }$$
11	8 10 9	co	$$class\left[0,\mathrm{+\infty }\right]$$
12	7 11 6	wf	$$wffm:s⟶\left[0,\mathrm{+\infty }\right]$$
13		c0	$$class\varnothing$$
14	13 6	cfv	$$classm\left(\varnothing \right)$$
15	14 8	wceq	$$wffm\left(\varnothing \right)=0$$
16		vx	$$setvarx$$
17	7	cpw	$$class𝒫s$$
18	16	cv	$$setvarx$$
19		cdom	$$class\preccurlyeq$$
20		com	$$class\mathrm{\omega }$$
21	18 20 19	wbr	$$wffx\preccurlyeq \mathrm{\omega }$$
22		vy	$$setvary$$
23	22	cv	$$setvary$$
24	22 18 23	wdisj	$$wff\underset{y\in x}{Disj}y$$
25	21 24	wa	$$wff\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)$$
26	18	cuni	$$class\bigcup x$$
27	26 6	cfv	$$classm\left(\bigcup x\right)$$
28	23 6	cfv	$$classm\left(y\right)$$
29	18 28 22	cesum	$$class\underset{y\in x}{{\sum }^{*}}m\left(y\right)$$
30	27 29	wceq	$$wffm\left(\bigcup x\right)=\underset{y\in x}{{\sum }^{*}}m\left(y\right)$$
31	25 30	wi	$$wff\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to m\left(\bigcup x\right)=\underset{y\in x}{{\sum }^{*}}m\left(y\right)\right)$$
32	31 16 17	wral	$$wff\forall x\in 𝒫s\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to m\left(\bigcup x\right)=\underset{y\in x}{{\sum }^{*}}m\left(y\right)\right)$$
33	12 15 32	w3a	$$wff\left(m:s⟶\left[0,\mathrm{+\infty }\right]\wedge m\left(\varnothing \right)=0\wedge \forall x\in 𝒫s\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to m\left(\bigcup x\right)=\underset{y\in x}{{\sum }^{*}}m\left(y\right)\right)\right)$$
34	33 5	cab	$$class\left\{m|\left(m:s⟶\left[0,\mathrm{+\infty }\right]\wedge m\left(\varnothing \right)=0\wedge \forall x\in 𝒫s\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to m\left(\bigcup x\right)=\underset{y\in x}{{\sum }^{*}}m\left(y\right)\right)\right)\right\}$$
35	1 4 34	cmpt	$$class\left(s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}⟼\left\{m|\left(m:s⟶\left[0,\mathrm{+\infty }\right]\wedge m\left(\varnothing \right)=0\wedge \forall x\in 𝒫s\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to m\left(\bigcup x\right)=\underset{y\in x}{{\sum }^{*}}m\left(y\right)\right)\right)\right\}\right)$$
36	0 35	wceq	$$wff\mathrm{measures}=\left(s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}⟼\left\{m|\left(m:s⟶\left[0,\mathrm{+\infty }\right]\wedge m\left(\varnothing \right)=0\wedge \forall x\in 𝒫s\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to m\left(\bigcup x\right)=\underset{y\in x}{{\sum }^{*}}m\left(y\right)\right)\right)\right\}\right)$$