Theorem isros

Description: The property of being a rings of sets, i.e. containing the empty set, and closed under finite union and set complement. (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	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)$$

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		eleq2	$$⊢s=S\to \left(\varnothing \in s\leftrightarrow \varnothing \in S\right)$$
3		eleq2	$$⊢s=S\to \left(x\cup y\in s\leftrightarrow x\cup y\in S\right)$$
4		eleq2	$$⊢s=S\to \left(x\setminus y\in s\leftrightarrow x\setminus y\in S\right)$$
5	3 4	anbi12d	$$⊢s=S\to \left(\left(x\cup y\in s\wedge x\setminus y\in s\right)\leftrightarrow \left(x\cup y\in S\wedge x\setminus y\in S\right)\right)$$
6	5	raleqbi1dv	$$⊢s=S\to \left(\forall y\in s\left(x\cup y\in s\wedge x\setminus y\in s\right)\leftrightarrow \forall y\in S\left(x\cup y\in S\wedge x\setminus y\in S\right)\right)$$
7	6	raleqbi1dv	$$⊢s=S\to \left(\forall x\in s\forall y\in s\left(x\cup y\in s\wedge x\setminus y\in s\right)\leftrightarrow \forall x\in S\forall y\in S\left(x\cup y\in S\wedge x\setminus y\in S\right)\right)$$
8	2 7	anbi12d	$$⊢s=S\to \left(\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)\leftrightarrow \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)$$
9	8 1	elrab2	$$⊢S\in Q\leftrightarrow \left(S\in 𝒫𝒫O\wedge \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)$$
10		3anass	$$⊢\left(S\in 𝒫𝒫O\wedge \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)\leftrightarrow \left(S\in 𝒫𝒫O\wedge \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)$$
11		uneq1	$$⊢x=u\to x\cup y=u\cup y$$
12	11	eleq1d	$$⊢x=u\to \left(x\cup y\in S\leftrightarrow u\cup y\in S\right)$$
13		difeq1	$$⊢x=u\to x\setminus y=u\setminus y$$
14	13	eleq1d	$$⊢x=u\to \left(x\setminus y\in S\leftrightarrow u\setminus y\in S\right)$$
15	12 14	anbi12d	$$⊢x=u\to \left(\left(x\cup y\in S\wedge x\setminus y\in S\right)\leftrightarrow \left(u\cup y\in S\wedge u\setminus y\in S\right)\right)$$
16		uneq2	$$⊢y=v\to u\cup y=u\cup v$$
17	16	eleq1d	$$⊢y=v\to \left(u\cup y\in S\leftrightarrow u\cup v\in S\right)$$
18		difeq2	$$⊢y=v\to u\setminus y=u\setminus v$$
19	18	eleq1d	$$⊢y=v\to \left(u\setminus y\in S\leftrightarrow u\setminus v\in S\right)$$
20	17 19	anbi12d	$$⊢y=v\to \left(\left(u\cup y\in S\wedge u\setminus y\in S\right)\leftrightarrow \left(u\cup v\in S\wedge u\setminus v\in S\right)\right)$$
21	15 20	cbvral2vw	$$⊢\forall x\in S\forall y\in S\left(x\cup y\in S\wedge x\setminus y\in S\right)\leftrightarrow \forall u\in S\forall v\in S\left(u\cup v\in S\wedge u\setminus v\in S\right)$$
22	21	3anbi3i	$$⊢\left(S\in 𝒫𝒫O\wedge \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)\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)$$
23	9 10 22	3bitr2i	$$⊢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)$$