# 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}\in \mathrm{sigAlgebra}\left({A}\right)\to {S}\subseteq 𝒫{A}$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{S}\in \mathrm{sigAlgebra}\left({A}\right)\to {S}\in \mathrm{V}$
2 issiga ${⊢}{S}\in \mathrm{V}\to \left({S}\in \mathrm{sigAlgebra}\left({A}\right)↔\left({S}\subseteq 𝒫{A}\wedge \left({A}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\right)$
3 2 biimpa ${⊢}\left({S}\in \mathrm{V}\wedge {S}\in \mathrm{sigAlgebra}\left({A}\right)\right)\to \left({S}\subseteq 𝒫{A}\wedge \left({A}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
4 1 3 mpancom ${⊢}{S}\in \mathrm{sigAlgebra}\left({A}\right)\to \left({S}\subseteq 𝒫{A}\wedge \left({A}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
5 4 simpld ${⊢}{S}\in \mathrm{sigAlgebra}\left({A}\right)\to {S}\subseteq 𝒫{A}$