# Metamath Proof Explorer

## 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}$