Theorem difunielsiga

Description: A sigma-algebra is closed under complement relative to its base set. This is immediate from the definition, see issiga , but the library states it nowhere in this form. (Contributed by Vincent Gonzalez, 17-Aug-2026)

	Ref	Expression
Assertion	difunielsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\right)\to \bigcup S\setminus A\in S$$

Proof

Step	Hyp	Ref	Expression
1		isrnsigau	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(S\subseteq 𝒫\bigcup S\wedge \left(\bigcup S\in S\wedge \forall x\in S\bigcup S\setminus x\in S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)\right)$$
2	1	simprd	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(\bigcup S\in S\wedge \forall x\in S\bigcup S\setminus x\in S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)$$
3	2	simp2d	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \forall x\in S\bigcup S\setminus x\in S$$
4		difeq2	$$⊢x=A\to \bigcup S\setminus x=\bigcup S\setminus A$$
5	4	eleq1d	$$⊢x=A\to \left(\bigcup S\setminus x\in S\leftrightarrow \bigcup S\setminus A\in S\right)$$
6	5	rspccva	$$⊢\left(\forall x\in S\bigcup S\setminus x\in S\wedge A\in S\right)\to \bigcup S\setminus A\in S$$
7	3 6	sylan	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\right)\to \bigcup S\setminus A\in S$$