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