Theorem saluni

Description: A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	saluni	⊢ ( 𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		dif0	⊢ ( ∪ 𝑆 ∖ ∅ ) = ∪ 𝑆
2		0sal	⊢ ( 𝑆 ∈ SAlg → ∅ ∈ 𝑆 )
3		saldifcl	⊢ ( ( 𝑆 ∈ SAlg ∧ ∅ ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ∅ ) ∈ 𝑆 )
4	2 3	mpdan	⊢ ( 𝑆 ∈ SAlg → ( ∪ 𝑆 ∖ ∅ ) ∈ 𝑆 )
5	1 4	eqeltrrid	⊢ ( 𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆 )