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 )