# 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}$
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 6, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://metamath.tirix.org/mpests/sigasspw", "fetch_time": 1721392281000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2024-30/segments/1720763514902.63/warc/CC-MAIN-20240719105029-20240719135029-00813.warc.gz", "warc_record_offset": 20534493, "warc_record_length": 2197, "token_count": 625, "char_count": 1470, "score": 3.53125, "int_score": 4, "crawl": "CC-MAIN-2024-30", "snapshot_type": "latest", "language": "en", "language_score": 0.351456880569458, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00063-of-00064.parquet"}