Definition df-prob

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprb	⊢ Prob
1		vp	⊢ 𝑝
2		cmeas	⊢ measures
3	2	crn	⊢ ran measures
4	3	cuni	⊢ ∪ ran measures
5	1	cv	⊢ 𝑝
6	5	cdm	⊢ dom 𝑝
7	6	cuni	⊢ ∪ dom 𝑝
8	7 5	cfv	⊢ ( 𝑝 ‘ ∪ dom 𝑝 )
9		c1	⊢ 1
10	8 9	wceq	⊢ ( 𝑝 ‘ ∪ dom 𝑝 ) = 1
11	10 1 4	crab	⊢ { 𝑝 ∈ ∪ ran measures ∣ ( 𝑝 ‘ ∪ dom 𝑝 ) = 1 }
12	0 11	wceq	⊢ Prob = { 𝑝 ∈ ∪ ran measures ∣ ( 𝑝 ‘ ∪ dom 𝑝 ) = 1 }