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 
|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )

Proof

Step Hyp Ref Expression
1 dfin4 
 |-  ( A i^i B ) = ( A \ ( A \ B ) )
2 difelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )
3 difelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ ( A \ B ) e. S ) -> ( A \ ( A \ B ) ) e. S )
4 2 3 syld3an3 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ ( A \ B ) ) e. S )
5 1 4 eqeltrid 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )