Metamath Proof Explorer

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 ⊢ φ → P ∈ Prob
Assertion unveldomd ⊢ φ → ⋃ dom ⁡ P ∈ dom ⁡ P

Proof

Step Hyp Ref Expression
1 unveldomd.1 ⊢ φ → P ∈ Prob
2 domprobsiga ⊢ P ∈ Prob → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
3 sgon ⊢ dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra → dom ⁡ P ∈ sigAlgebra ⁡ ⋃ dom ⁡ P
4 baselsiga ⊢ dom ⁡ P ∈ sigAlgebra ⁡ ⋃ dom ⁡ P → ⋃ dom ⁡ P ∈ dom ⁡ P
5 1 2 3 4 4syl ⊢ φ → ⋃ dom ⁡ P ∈ dom ⁡ P