Definition df-prob 29797

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

Assertion

Ref	Expression
df-prob	⊢ Prob = {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}

Detailed syntax breakdown of Definition df-prob

Step	Hyp	Ref	Expression
1		cprb 29796	. 2 class Prob
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1474	. . . . . . 7 class 𝑝
4	3	cdm 5038	. . . . . 6 class dom 𝑝
5	4	cuni 4372	. . . . 5 class ∪ dom 𝑝
6	5, 3	cfv 5804	. . . 4 class (𝑝‘∪ dom 𝑝)
7		c1 9816	. . . 4 class 1
8	6, 7	wceq 1475	. . 3 wff (𝑝‘∪ dom 𝑝) = 1
9		cmeas 29585	. . . . 5 class measures
10	9	crn 5039	. . . 4 class ran measures
11	10	cuni 4372	. . 3 class ∪ ran measures
12	8, 2, 11	crab 2900	. 2 class {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}
13	1, 12	wceq 1475	1 wff Prob = {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}

This definition is referenced by:  elprob  29798