Definition df-prob 33407

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 33406	. 2 class Prob
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1541	. . . . . . 7 class 𝑝
4	3	cdm 5677	. . . . . 6 class dom 𝑝
5	4	cuni 4909	. . . . 5 class ∪ dom 𝑝
6	5, 3	cfv 6544	. . . 4 class (𝑝‘∪ dom 𝑝)
7		c1 11111	. . . 4 class 1
8	6, 7	wceq 1542	. . 3 wff (𝑝‘∪ dom 𝑝) = 1
9		cmeas 33193	. . . . 5 class measures
10	9	crn 5678	. . . 4 class ran measures
11	10	cuni 4909	. . 3 class ∪ ran measures
12	8, 2, 11	crab 3433	. 2 class {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}
13	1, 12	wceq 1542	1 wff Prob = {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}

This definition is referenced by:  elprob  33408