Theorem srossspw

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

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