Metamath Proof Explorer

Theorem domprobmeas

Description: A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016)

Ref Expression
Assertion domprobmeas ⊢ P ∈ Prob → P ∈ measures ⁡ dom ⁡ P

Proof

Step Hyp Ref Expression
1 elprob ⊢ P ∈ Prob ↔ P ∈ ⋃ ran ⁡ measures ∧ P ⁡ ⋃ dom ⁡ P = 1
2 1 simplbi ⊢ P ∈ Prob → P ∈ ⋃ ran ⁡ measures
3 measbasedom ⊢ P ∈ ⋃ ran ⁡ measures ↔ P ∈ measures ⁡ dom ⁡ P
4 2 3 sylib ⊢ P ∈ Prob → P ∈ measures ⁡ dom ⁡ P