Theorem difelsiga

Description: A sigma-algebra is closed under class differences. The proof goes through difunielsiga and unelsiga rather than countable intersection, and so does not use ax-ac . (Contributed by Thierry Arnoux, 13-Sep-2016) (Proof shortened by Vincent Gonzalez, 17-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		difun1	$$⊢\bigcup S\setminus \left(\left(\bigcup S\setminus A\right)\cup B\right)=\left(\bigcup S\setminus \left(\bigcup S\setminus A\right)\right)\setminus B$$
2	1	a1i	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \bigcup S\setminus \left(\left(\bigcup S\setminus A\right)\cup B\right)=\left(\bigcup S\setminus \left(\bigcup S\setminus A\right)\right)\setminus B$$
3		simp1	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
4		simp2	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\in S$$
5		elsigass	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\right)\to A\subseteq \bigcup S$$
6	3 4 5	syl2anc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\subseteq \bigcup S$$
7		dfss4	$$⊢A\subseteq \bigcup S\leftrightarrow \bigcup S\setminus \left(\bigcup S\setminus A\right)=A$$
8	6 7	sylib	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \bigcup S\setminus \left(\bigcup S\setminus A\right)=A$$
9	8	difeq1d	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \left(\bigcup S\setminus \left(\bigcup S\setminus A\right)\right)\setminus B=A\setminus B$$
10	2 9	eqtrd	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \bigcup S\setminus \left(\left(\bigcup S\setminus A\right)\cup B\right)=A\setminus B$$
11		difunielsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\right)\to \bigcup S\setminus A\in S$$
12	3 4 11	syl2anc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \bigcup S\setminus A\in S$$
13		simp3	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to B\in S$$
14		unelsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup S\setminus A\in S\wedge B\in S\right)\to \left(\bigcup S\setminus A\right)\cup B\in S$$
15	3 12 13 14	syl3anc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \left(\bigcup S\setminus A\right)\cup B\in S$$
16		difunielsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \left(\bigcup S\setminus A\right)\cup B\in S\right)\to \bigcup S\setminus \left(\left(\bigcup S\setminus A\right)\cup B\right)\in S$$
17	3 15 16	syl2anc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \bigcup S\setminus \left(\left(\bigcup S\setminus A\right)\cup B\right)\in S$$
18	10 17	eqeltrrd	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\setminus B\in S$$