Theorem inelsiga

Description: A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		dfin4	$$⊢A\cap B=A\setminus \left(A\setminus B\right)$$
2		difelsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\setminus B\in S$$
3		difelsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge A\setminus B\in S\right)\to A\setminus \left(A\setminus B\right)\in S$$
4	2 3	syld3an3	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\setminus \left(A\setminus B\right)\in S$$
5	1 4	eqeltrid	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\cap B\in S$$