Theorem rossspw

Description: A ring of sets is a collection of subsets of O . (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	rossspw	$$⊢S\in Q\to S\subseteq 𝒫O$$

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	simp1bi	$$⊢S\in Q\to S\in 𝒫𝒫O$$
4	3	elpwid	$$⊢S\in Q\to S\subseteq 𝒫O$$