Description: A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | sgon | ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ∪ 𝑆 = ∪ 𝑆 | |
2 | issgon | ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) ↔ ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑆 = ∪ 𝑆 ) ) | |
3 | 2 | biimpri | ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑆 = ∪ 𝑆 ) → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) ) |
4 | 1 3 | mpan2 | ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) ) |