Definition df-prob

Description: Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016)

	Ref	Expression
Assertion	df-prob	$$⊢\mathrm{Prob}=\left\{p\in \bigcup \mathrm{ran}\mathrm{measures}|p\left(\bigcup \mathrm{dom}p\right)=1\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprb	$$class\mathrm{Prob}$$
1		vp	$$setvarp$$
2		cmeas	$$class\mathrm{measures}$$
3	2	crn	$$class\mathrm{ran}\mathrm{measures}$$
4	3	cuni	$$class\bigcup \mathrm{ran}\mathrm{measures}$$
5	1	cv	$$setvarp$$
6	5	cdm	$$class\mathrm{dom}p$$
7	6	cuni	$$class\bigcup \mathrm{dom}p$$
8	7 5	cfv	$$classp\left(\bigcup \mathrm{dom}p\right)$$
9		c1	$$class1$$
10	8 9	wceq	$$wffp\left(\bigcup \mathrm{dom}p\right)=1$$
11	10 1 4	crab	$$class\left\{p\in \bigcup \mathrm{ran}\mathrm{measures}|p\left(\bigcup \mathrm{dom}p\right)=1\right\}$$
12	0 11	wceq	$$wff\mathrm{Prob}=\left\{p\in \bigcup \mathrm{ran}\mathrm{measures}|p\left(\bigcup \mathrm{dom}p\right)=1\right\}$$