Theorem inelsiga

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

	Ref	Expression
Assertion	inelsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		dfin4	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) )
2		difelsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 )
3		difelsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ∈ 𝑆 )
4	2 3	syld3an3	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ∈ 𝑆 )
5	1 4	eqeltrid	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 )