Metamath Proof Explorer


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 ‘ 𝐴 ) → 𝑆 ⊆ 𝒫 𝐴 )