# Metamath Proof Explorer

## Theorem elsigagen2

Description: Any countable union of elements of a set is also in the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 17-Sep-2017)

Ref Expression
Assertion elsigagen2 ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to \bigcup {B}\in 𝛔\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to {A}\in {V}$
2 1 sgsiga ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to 𝛔\left({A}\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 sssigagen ${⊢}{A}\in {V}\to {A}\subseteq 𝛔\left({A}\right)$
4 sspw ${⊢}{A}\subseteq 𝛔\left({A}\right)\to 𝒫{A}\subseteq 𝒫𝛔\left({A}\right)$
5 1 3 4 3syl ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to 𝒫{A}\subseteq 𝒫𝛔\left({A}\right)$
6 simp2 ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to {B}\subseteq {A}$
7 simp3 ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to {B}\preccurlyeq \mathrm{\omega }$
8 ctex ${⊢}{B}\preccurlyeq \mathrm{\omega }\to {B}\in \mathrm{V}$
9 elpwg ${⊢}{B}\in \mathrm{V}\to \left({B}\in 𝒫{A}↔{B}\subseteq {A}\right)$
10 7 8 9 3syl ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to \left({B}\in 𝒫{A}↔{B}\subseteq {A}\right)$
11 6 10 mpbird ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to {B}\in 𝒫{A}$
12 5 11 sseldd ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to {B}\in 𝒫𝛔\left({A}\right)$
13 sigaclcu ${⊢}\left(𝛔\left({A}\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {B}\in 𝒫𝛔\left({A}\right)\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to \bigcup {B}\in 𝛔\left({A}\right)$
14 2 12 7 13 syl3anc ${⊢}\left({A}\in {V}\wedge {B}\subseteq {A}\wedge {B}\preccurlyeq \mathrm{\omega }\right)\to \bigcup {B}\in 𝛔\left({A}\right)$