Theorem sigasspw

Description: A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017)

	Ref	Expression
Assertion	sigasspw	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) → 𝑆 ⊆ 𝒫 𝐴 )

Proof

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