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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → ∪ 𝐵 ∈ ( sigaGen ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → 𝐴 ∈ 𝑉 )
2	1	sgsiga	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → ( sigaGen ‘ 𝐴 ) ∈ ∪ ran sigAlgebra )
3		sssigagen	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( sigaGen ‘ 𝐴 ) )
4		sspw	⊢ ( 𝐴 ⊆ ( sigaGen ‘ 𝐴 ) → 𝒫 𝐴 ⊆ 𝒫 ( sigaGen ‘ 𝐴 ) )
5	1 3 4	3syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → 𝒫 𝐴 ⊆ 𝒫 ( sigaGen ‘ 𝐴 ) )
6		simp2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → 𝐵 ⊆ 𝐴 )
7		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → 𝐵 ≼ ω )
8		ctex	⊢ ( 𝐵 ≼ ω → 𝐵 ∈ V )
9		elpwg	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
10	7 8 9	3syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
11	6 10	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → 𝐵 ∈ 𝒫 𝐴 )
12	5 11	sseldd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → 𝐵 ∈ 𝒫 ( sigaGen ‘ 𝐴 ) )
13		sigaclcu	⊢ ( ( ( sigaGen ‘ 𝐴 ) ∈ ∪ ran sigAlgebra ∧ 𝐵 ∈ 𝒫 ( sigaGen ‘ 𝐴 ) ∧ 𝐵 ≼ ω ) → ∪ 𝐵 ∈ ( sigaGen ‘ 𝐴 ) )
14	2 12 7 13	syl3anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω ) → ∪ 𝐵 ∈ ( sigaGen ‘ 𝐴 ) )