Theorem salincld

Description: The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	salincld.1	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	salincld.2	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
	salincld.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
Assertion	salincld	⊢ ( 𝜑 → ( 𝐸 ∩ 𝐹 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		salincld.1	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		salincld.2	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
3		salincld.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
4		salincl	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) ∈ 𝑆 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( 𝐸 ∩ 𝐹 ) ∈ 𝑆 )