Theorem baselsiga

Description: A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016)

	Ref	Expression
Assertion	baselsiga	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) → 𝐴 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) → 𝑆 ∈ V )
2		issiga	⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ↔ ( 𝑆 ⊆ 𝒫 𝐴 ∧ ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
3	2	simplbda	⊢ ( ( 𝑆 ∈ V ∧ 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ) → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
4	3	simp1d	⊢ ( ( 𝑆 ∈ V ∧ 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ) → 𝐴 ∈ 𝑆 )
5	1 4	mpancom	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) → 𝐴 ∈ 𝑆 )