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	|- Prob = { p e. U. ran measures | ( p ` U. dom p ) = 1 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprb	|- Prob
1		vp	|- p
2		cmeas	|- measures
3	2	crn	|- ran measures
4	3	cuni	|- U. ran measures
5	1	cv	|- p
6	5	cdm	|- dom p
7	6	cuni	|- U. dom p
8	7 5	cfv	|- ( p ` U. dom p )
9		c1	|- 1
10	8 9	wceq	|- ( p ` U. dom p ) = 1
11	10 1 4	crab	|- { p e. U. ran measures | ( p ` U. dom p ) = 1 }
12	0 11	wceq	|- Prob = { p e. U. ran measures | ( p ` U. dom p ) = 1 }