Theorem 0elsros

Description: A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypothesis	issros.1	$$⊢N=\left\{s\in 𝒫𝒫O|\left(\varnothing \in s\wedge \forall x\in s\forall y\in s\left(x\cap y\in s\wedge \exists z\in 𝒫s\left(z\in \mathrm{Fin}\wedge \underset{t\in z}{Disj}t\wedge x\setminus y=\bigcup z\right)\right)\right)\right\}$$
Assertion	0elsros	$$⊢S\in N\to \varnothing \in S$$

Proof

Step	Hyp	Ref	Expression
1		issros.1	$$⊢N=\left\{s\in 𝒫𝒫O|\left(\varnothing \in s\wedge \forall x\in s\forall y\in s\left(x\cap y\in s\wedge \exists z\in 𝒫s\left(z\in \mathrm{Fin}\wedge \underset{t\in z}{Disj}t\wedge x\setminus y=\bigcup z\right)\right)\right)\right\}$$
2	1	issros	$$⊢S\in N\leftrightarrow \left(S\in 𝒫𝒫O\wedge \varnothing \in S\wedge \forall x\in S\forall y\in S\left(x\cap y\in S\wedge \exists z\in 𝒫S\left(z\in \mathrm{Fin}\wedge \underset{t\in z}{Disj}t\wedge x\setminus y=\bigcup z\right)\right)\right)$$
3	2	simp2bi	$$⊢S\in N\to \varnothing \in S$$