Theorem 0elros

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

	Ref	Expression
Hypothesis	isros.1	$$⊢Q=\left\{s\in 𝒫𝒫O|\left(\varnothing \in s\wedge \forall x\in s\forall y\in s\left(x\cup y\in s\wedge x\setminus y\in s\right)\right)\right\}$$
Assertion	0elros	$$⊢S\in Q\to \varnothing \in S$$

Proof

Step	Hyp	Ref	Expression
1		isros.1	$$⊢Q=\left\{s\in 𝒫𝒫O|\left(\varnothing \in s\wedge \forall x\in s\forall y\in s\left(x\cup y\in s\wedge x\setminus y\in s\right)\right)\right\}$$
2	1	isros	$$⊢S\in Q\leftrightarrow \left(S\in 𝒫𝒫O\wedge \varnothing \in S\wedge \forall u\in S\forall v\in S\left(u\cup v\in S\wedge u\setminus v\in S\right)\right)$$
3	2	simp2bi	$$⊢S\in Q\to \varnothing \in S$$