Theorem 0sal

Description: The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	0sal	⊢ ( 𝑆 ∈ SAlg → ∅ ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		issal	⊢ ( 𝑆 ∈ SAlg → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
2	1	ibi	⊢ ( 𝑆 ∈ SAlg → ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) )
3	2	simp1d	⊢ ( 𝑆 ∈ SAlg → ∅ ∈ 𝑆 )