Theorem salincl

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

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

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\cap F=E\cap F$$
2		inss1	$$⊢E\cap F\subseteq E$$
3	2	a1i	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to E\cap F\subseteq E$$
4		elssuni	$$⊢E\in S\to E\subseteq \bigcup S$$
5	4	adantl	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to E\subseteq \bigcup S$$
6	3 5	sstrd	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to E\cap F\subseteq \bigcup S$$
7		dfss4	$$⊢E\cap F\subseteq \bigcup S\leftrightarrow \bigcup S\setminus \left(\bigcup S\setminus \left(E\cap F\right)\right)=E\cap F$$
8	6 7	sylib	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to \bigcup S\setminus \left(\bigcup S\setminus \left(E\cap F\right)\right)=E\cap F$$
9	8	eqcomd	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to E\cap F=\bigcup S\setminus \left(\bigcup S\setminus \left(E\cap F\right)\right)$$
10	9	3adant3	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\cap F=\bigcup S\setminus \left(\bigcup S\setminus \left(E\cap F\right)\right)$$
11		difindi	$$⊢\bigcup S\setminus \left(E\cap F\right)=\left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)$$
12	11	difeq2i	$$⊢\bigcup S\setminus \left(\bigcup S\setminus \left(E\cap F\right)\right)=\bigcup S\setminus \left(\left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)\right)$$
13	12	a1i	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to \bigcup S\setminus \left(\bigcup S\setminus \left(E\cap F\right)\right)=\bigcup S\setminus \left(\left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)\right)$$
14	1 10 13	3eqtrd	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\cap F=\bigcup S\setminus \left(\left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)\right)$$
15		simp1	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to S\in \mathrm{SAlg}$$
16		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to \bigcup S\setminus E\in S$$
17	16	3adant3	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to \bigcup S\setminus E\in S$$
18		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge F\in S\right)\to \bigcup S\setminus F\in S$$
19	18	3adant2	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to \bigcup S\setminus F\in S$$
20		saluncl	$$⊢\left(S\in \mathrm{SAlg}\wedge \bigcup S\setminus E\in S\wedge \bigcup S\setminus F\in S\right)\to \left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)\in S$$
21	15 17 19 20	syl3anc	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to \left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)\in S$$
22		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge \left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)\in S\right)\to \bigcup S\setminus \left(\left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)\right)\in S$$
23	15 21 22	syl2anc	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to \bigcup S\setminus \left(\left(\bigcup S\setminus E\right)\cup \left(\bigcup S\setminus F\right)\right)\in S$$
24	14 23	eqeltrd	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\wedge F\in S\right)\to E\cap F\in S$$