Metamath Proof Explorer


Theorem elsigass

Description: An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017)

Ref Expression
Assertion elsigass
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A C_ U. S )

Proof

Step Hyp Ref Expression
1 sgon
 |-  ( S e. U. ran sigAlgebra -> S e. ( sigAlgebra ` U. S ) )
2 sigasspw
 |-  ( S e. ( sigAlgebra ` U. S ) -> S C_ ~P U. S )
3 1 2 syl
 |-  ( S e. U. ran sigAlgebra -> S C_ ~P U. S )
4 3 sselda
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A e. ~P U. S )
5 4 elpwid
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A C_ U. S )