Theorem elprob

Description: The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016)

	Ref	Expression
Assertion	elprob	$$⊢P\in \mathrm{Prob}\leftrightarrow \left(P\in \bigcup \mathrm{ran}\mathrm{measures}\wedge P\left(\bigcup \mathrm{dom}P\right)=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢p=P\to p=P$$
2		dmeq	$$⊢p=P\to \mathrm{dom}p=\mathrm{dom}P$$
3	2	unieqd	$$⊢p=P\to \bigcup \mathrm{dom}p=\bigcup \mathrm{dom}P$$
4	1 3	fveq12d	$$⊢p=P\to p\left(\bigcup \mathrm{dom}p\right)=P\left(\bigcup \mathrm{dom}P\right)$$
5	4	eqeq1d	$$⊢p=P\to \left(p\left(\bigcup \mathrm{dom}p\right)=1\leftrightarrow P\left(\bigcup \mathrm{dom}P\right)=1\right)$$
6		df-prob	$$⊢\mathrm{Prob}=\left\{p\in \bigcup \mathrm{ran}\mathrm{measures}|p\left(\bigcup \mathrm{dom}p\right)=1\right\}$$
7	5 6	elrab2	$$⊢P\in \mathrm{Prob}\leftrightarrow \left(P\in \bigcup \mathrm{ran}\mathrm{measures}\wedge P\left(\bigcup \mathrm{dom}P\right)=1\right)$$