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 e. Prob -> (/) e. dom P )

Proof

Step Hyp Ref Expression
1 domprobsiga 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
2 0elsiga 
 |-  ( dom P e. U. ran sigAlgebra -> (/) e. dom P )
3 1 2 syl 
 |-  ( P e. Prob -> (/) e. dom P )