Definition df-prob 35023

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 35022	. 2 class Prob
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1569	. . . . . . 7 class 𝑝
4	3	cdm 5651	. . . . . 6 class dom 𝑝
5	4	cuni 4867	. . . . 5 class ∪ dom 𝑝
6	5, 3	cfv 6531	. . . 4 class (𝑝‘∪ dom 𝑝)
7		c1 11182	. . . 4 class 1
8	6, 7	wceq 1570	. . 3 wff (𝑝‘∪ dom 𝑝) = 1
9		cmeas 34810	. . . . 5 class measures
10	9	crn 5652	. . . 4 class ran measures
11	10	cuni 4867	. . 3 class ∪ ran measures
12	8, 2, 11	crab 3413	. 2 class {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}
13	1, 12	wceq 1570	1 wff Prob = {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}

This definition is used by:  elprob  35024