Theorem inelros

Description: A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-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	inelros	$$⊢\left(S\in Q\wedge A\in S\wedge B\in S\right)\to A\cap B\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		dfin4	$$⊢A\cap B=A\setminus \left(A\setminus B\right)$$
3	1	difelros	$$⊢\left(S\in Q\wedge A\in S\wedge B\in S\right)\to A\setminus B\in S$$
4	1	difelros	$$⊢\left(S\in Q\wedge A\in S\wedge A\setminus B\in S\right)\to A\setminus \left(A\setminus B\right)\in S$$
5	3 4	syld3an3	$$⊢\left(S\in Q\wedge A\in S\wedge B\in S\right)\to A\setminus \left(A\setminus B\right)\in S$$
6	2 5	eqeltrid	$$⊢\left(S\in Q\wedge A\in S\wedge B\in S\right)\to A\cap B\in S$$