Theorem unveldomd

Description: The universe is an element of the domain of the probability, the universe (entire probability space) being U. dom P in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017)

	Ref	Expression
Hypothesis	unveldomd.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
Assertion	unveldomd	⊢ ( 𝜑 → ∪ dom 𝑃 ∈ dom 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		unveldomd.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		domprobsiga	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
3		sgon	⊢ ( dom 𝑃 ∈ ∪ ran sigAlgebra → dom 𝑃 ∈ ( sigAlgebra ‘ ∪ dom 𝑃 ) )
4		baselsiga	⊢ ( dom 𝑃 ∈ ( sigAlgebra ‘ ∪ dom 𝑃 ) → ∪ dom 𝑃 ∈ dom 𝑃 )
5	1 2 3 4	4syl	⊢ ( 𝜑 → ∪ dom 𝑃 ∈ dom 𝑃 )