Definition df-prob 31668

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 31667	. 2 class Prob
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1536	. . . . . . 7 class 𝑝
4	3	cdm 5557	. . . . . 6 class dom 𝑝
5	4	cuni 4840	. . . . 5 class ∪ dom 𝑝
6	5, 3	cfv 6357	. . . 4 class (𝑝‘∪ dom 𝑝)
7		c1 10540	. . . 4 class 1
8	6, 7	wceq 1537	. . 3 wff (𝑝‘∪ dom 𝑝) = 1
9		cmeas 31456	. . . . 5 class measures
10	9	crn 5558	. . . 4 class ran measures
11	10	cuni 4840	. . 3 class ∪ ran measures
12	8, 2, 11	crab 3144	. 2 class {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}
13	1, 12	wceq 1537	1 wff Prob = {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}

This definition is referenced by:  elprob  31669