Definition df-prob 32354

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 32353	. 2 class Prob
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1540	. . . . . . 7 class 𝑝
4	3	cdm 5588	. . . . . 6 class dom 𝑝
5	4	cuni 4844	. . . . 5 class ∪ dom 𝑝
6	5, 3	cfv 6430	. . . 4 class (𝑝‘∪ dom 𝑝)
7		c1 10856	. . . 4 class 1
8	6, 7	wceq 1541	. . 3 wff (𝑝‘∪ dom 𝑝) = 1
9		cmeas 32142	. . . . 5 class measures
10	9	crn 5589	. . . 4 class ran measures
11	10	cuni 4844	. . 3 class ∪ ran measures
12	8, 2, 11	crab 3069	. 2 class {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}
13	1, 12	wceq 1541	1 wff Prob = {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}

This definition is referenced by:  elprob  32355