Metamath Proof Explorer

Theorem sigasspw

Description: A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017)

Ref Expression
Assertion sigasspw 
|- ( S e. ( sigAlgebra ` A ) -> S C_ ~P A )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( S e. ( sigAlgebra ` A ) -> S e. _V )
2 issiga 
 |-  ( S e. _V -> ( S e. ( sigAlgebra ` A ) <-> ( S C_ ~P A /\ ( A e. S /\ A. x e. S ( A \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) ) )
3 2 biimpa 
 |-  ( ( S e. _V /\ S e. ( sigAlgebra ` A ) ) -> ( S C_ ~P A /\ ( A e. S /\ A. x e. S ( A \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
4 1 3 mpancom 
 |-  ( S e. ( sigAlgebra ` A ) -> ( S C_ ~P A /\ ( A e. S /\ A. x e. S ( A \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
5 4 simpld 
 |-  ( S e. ( sigAlgebra ` A ) -> S C_ ~P A )