Step |
Hyp |
Ref |
Expression |
1 |
|
ssexg |
⊢ ( ( 𝐴 ⊆ 𝑆 ∧ 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ) → 𝐴 ∈ V ) |
2 |
1
|
ancoms |
⊢ ( ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∧ 𝐴 ⊆ 𝑆 ) → 𝐴 ∈ V ) |
3 |
|
sigagenval |
⊢ ( 𝐴 ∈ V → ( sigaGen ‘ 𝐴 ) = ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ) |
4 |
2 3
|
syl |
⊢ ( ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∧ 𝐴 ⊆ 𝑆 ) → ( sigaGen ‘ 𝐴 ) = ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ) |
5 |
|
sseq2 |
⊢ ( 𝑠 = 𝑆 → ( 𝐴 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑆 ) ) |
6 |
5
|
intminss |
⊢ ( ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∧ 𝐴 ⊆ 𝑆 ) → ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ⊆ 𝑆 ) |
7 |
4 6
|
eqsstrd |
⊢ ( ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∧ 𝐴 ⊆ 𝑆 ) → ( sigaGen ‘ 𝐴 ) ⊆ 𝑆 ) |