# Metamath Proof Explorer

## Theorem baselsiga

Description: A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016)

Ref Expression
Assertion baselsiga ${⊢}{S}\in \mathrm{sigAlgebra}\left({A}\right)\to {A}\in {S}$

### 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 simplbda ${⊢}\left({S}\in \mathrm{V}\wedge {S}\in \mathrm{sigAlgebra}\left({A}\right)\right)\to \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)$
4 3 simp1d ${⊢}\left({S}\in \mathrm{V}\wedge {S}\in \mathrm{sigAlgebra}\left({A}\right)\right)\to {A}\in {S}$
5 1 4 mpancom ${⊢}{S}\in \mathrm{sigAlgebra}\left({A}\right)\to {A}\in {S}$