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 ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → ⋃ B ∈ 𝛔 ⁡ A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → A ∈ V
2 1 sgsiga ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → 𝛔 ⁡ A ∈ ⋃ ran ⁡ sigAlgebra
3 sssigagen ⊢ A ∈ V → A ⊆ 𝛔 ⁡ A
4 sspw ⊢ A ⊆ 𝛔 ⁡ A → 𝒫 A ⊆ 𝒫 𝛔 ⁡ A
5 1 3 4 3syl ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → 𝒫 A ⊆ 𝒫 𝛔 ⁡ A
6 simp2 ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → B ⊆ A
7 simp3 ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → B ≼ ω
8 ctex ⊢ B ≼ ω → B ∈ V
9 elpwg ⊢ B ∈ V → B ∈ 𝒫 A ↔ B ⊆ A
10 7 8 9 3syl ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → B ∈ 𝒫 A ↔ B ⊆ A
11 6 10 mpbird ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → B ∈ 𝒫 A
12 5 11 sseldd ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → B ∈ 𝒫 𝛔 ⁡ A
13 sigaclcu ⊢ 𝛔 ⁡ A ∈ ⋃ ran ⁡ sigAlgebra ∧ B ∈ 𝒫 𝛔 ⁡ A ∧ B ≼ ω → ⋃ B ∈ 𝛔 ⁡ A
14 2 12 7 13 syl3anc ⊢ A ∈ V ∧ B ⊆ A ∧ B ≼ ω → ⋃ B ∈ 𝛔 ⁡ A