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	⊢ ( 𝑃 ∈ Prob → ∅ ∈ dom 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		domprobsiga	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
2		0elsiga	⊢ ( dom 𝑃 ∈ ∪ ran sigAlgebra → ∅ ∈ dom 𝑃 )
3	1 2	syl	⊢ ( 𝑃 ∈ Prob → ∅ ∈ dom 𝑃 )