Metamath Proof Explorer

Theorem unielsiga

Description: A sigma-algebra contains its universe set. (Contributed by Thierry Arnoux, 13-Feb-2017) (Shortened by Thierry Arnoux, 6-Jun-2017.)

Ref Expression
Assertion unielsiga 
|- ( S e. U. ran sigAlgebra -> U. S e. S )

Proof

Step Hyp Ref Expression
1 sgon 
 |-  ( S e. U. ran sigAlgebra -> S e. ( sigAlgebra ` U. S ) )
2 baselsiga 
 |-  ( S e. ( sigAlgebra ` U. S ) -> U. S e. S )
3 1 2 syl 
 |-  ( S e. U. ran sigAlgebra -> U. S e. S )