Theorem saluncld

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

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

Proof

Step	Hyp	Ref	Expression
1		saluncld.1	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		saluncld.2	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
3		saluncld.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
4		saluncl	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∪ 𝐹 ) ∈ 𝑆 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ∈ 𝑆 )