Theorem saldifcl2

Description: The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		indif2	$$⊢E\cap \left(\bigcup S\setminus F\right)=\left(E\cap \bigcup S\right)\setminus F$$
2	1	a1i	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\cap \left(\bigcup S\setminus F\right)=\left(E\cap \bigcup S\right)\setminus F$$
3		elssuni	$$⊢E\in S\to E\subseteq \bigcup S$$
4		df-ss	$$⊢E\subseteq \bigcup S\leftrightarrow E\cap \bigcup S=E$$
5	3 4	sylib	$$⊢E\in S\to E\cap \bigcup S=E$$
6	5	difeq1d	$$⊢E\in S\to \left(E\cap \bigcup S\right)\setminus F=E\setminus F$$
7	6	3ad2ant2	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to \left(E\cap \bigcup S\right)\setminus F=E\setminus F$$
8	2 7	eqtr2d	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\setminus F=E\cap \left(\bigcup S\setminus F\right)$$
9		simp1	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to S\in \mathrm{SAlg}$$
10		simp2	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\in S$$
11		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge F\in S\right)\to \bigcup S\setminus F\in S$$
12	11	3adant2	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to \bigcup S\setminus F\in S$$
13		salincl	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge \bigcup S\setminus F\in S\right)\to E\cap \left(\bigcup S\setminus F\right)\in S$$
14	9 10 12 13	syl3anc	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\cap \left(\bigcup S\setminus F\right)\in S$$
15	8 14	eqeltrd	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\setminus F\in S$$