Theorem saldifcl

Description: The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to \bigcup S\setminus E\in S$$

Proof

Step	Hyp	Ref	Expression
1		difeq2	$$⊢y=E\to \bigcup S\setminus y=\bigcup S\setminus E$$
2	1	eleq1d	$$⊢y=E\to \left(\bigcup S\setminus y\in S\leftrightarrow \bigcup S\setminus E\in S\right)$$
3		issal	$$⊢S\in \mathrm{SAlg}\to \left(S\in \mathrm{SAlg}\leftrightarrow \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)\right)$$
4	3	ibi	$$⊢S\in \mathrm{SAlg}\to \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)$$
5	4	simp2d	$$⊢S\in \mathrm{SAlg}\to \forall y\in S\bigcup S\setminus y\in S$$
6	5	adantr	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to \forall y\in S\bigcup S\setminus y\in S$$
7		simpr	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to E\in S$$
8	2 6 7	rspcdva	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to \bigcup S\setminus E\in S$$