Metamath Proof Explorer

Theorem nuleldmp

Description: The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017)

Ref Expression
Assertion nuleldmp ⊢ P ∈ Prob → ∅ ∈ dom ⁡ P

Proof

Step Hyp Ref Expression
1 domprobsiga ⊢ P ∈ Prob → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
2 0elsiga ⊢ dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra → ∅ ∈ dom ⁡ P
3 1 2 syl ⊢ P ∈ Prob → ∅ ∈ dom ⁡ P