Metamath Proof Explorer

Theorem elrnsiga

Description: Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017)

Ref Expression
Assertion elrnsiga 
|- ( S e. ( sigAlgebra ` O ) -> S e. U. ran sigAlgebra )

Proof

Step Hyp Ref Expression
1 fvssunirn 
 |-  ( sigAlgebra ` O ) C_ U. ran sigAlgebra
2 1 sseli 
 |-  ( S e. ( sigAlgebra ` O ) -> S e. U. ran sigAlgebra )