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 
|- ( ph -> P e. Prob )
Assertion unveldomd 
|- ( ph -> U. dom P e. dom P )

Proof

Step Hyp Ref Expression
1 unveldomd.1 
 |-  ( ph -> P e. Prob )
2 domprobsiga 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
3 sgon 
 |-  ( dom P e. U. ran sigAlgebra -> dom P e. ( sigAlgebra ` U. dom P ) )
4 baselsiga 
 |-  ( dom P e. ( sigAlgebra ` U. dom P ) -> U. dom P e. dom P )
5 1 2 3 4 4syl 
 |-  ( ph -> U. dom P e. dom P )