Theorem elprob

Description: The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016)

	Ref	Expression
Assertion	elprob	⊢ ( 𝑃 ∈ Prob ↔ ( 𝑃 ∈ ∪ ran measures ∧ ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑝 = 𝑃 → 𝑝 = 𝑃 )
2		dmeq	⊢ ( 𝑝 = 𝑃 → dom 𝑝 = dom 𝑃 )
3	2	unieqd	⊢ ( 𝑝 = 𝑃 → ∪ dom 𝑝 = ∪ dom 𝑃 )
4	1 3	fveq12d	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ ∪ dom 𝑝 ) = ( 𝑃 ‘ ∪ dom 𝑃 ) )
5	4	eqeq1d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ ∪ dom 𝑝 ) = 1 ↔ ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 ) )
6		df-prob	⊢ Prob = { 𝑝 ∈ ∪ ran measures ∣ ( 𝑝 ‘ ∪ dom 𝑝 ) = 1 }
7	5 6	elrab2	⊢ ( 𝑃 ∈ Prob ↔ ( 𝑃 ∈ ∪ ran measures ∧ ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 ) )