Theorem 0sal

Description: The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	0sal	$$⊢S\in \mathrm{SAlg}\to \varnothing \in S$$

Proof

Step	Hyp	Ref	Expression
1		issal	$$⊢S\in \mathrm{SAlg}\to \left(S\in \mathrm{SAlg}\leftrightarrow \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)\right)$$
2	1	ibi	$$⊢S\in \mathrm{SAlg}\to \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)$$
3	2	simp1d	$$⊢S\in \mathrm{SAlg}\to \varnothing \in S$$