Theorem sigaclcu

Description: A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016)

	Ref	Expression
Assertion	sigaclcu	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω ) → ∪ 𝐴 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω ) → 𝐴 ∈ 𝒫 𝑆 )
2		isrnsiga	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra ↔ ( 𝑆 ∈ V ∧ ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
3	2	simprbi	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
4		simpr3	⊢ ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
5	4	exlimiv	⊢ ( ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
6	3 5	syl	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
7	6	3ad2ant1	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω ) → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
8		simp3	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω ) → 𝐴 ≼ ω )
9		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≼ ω ↔ 𝐴 ≼ ω ) )
10		unieq	⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 )
11	10	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ∪ 𝑥 ∈ 𝑆 ↔ ∪ 𝐴 ∈ 𝑆 ) )
12	9 11	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ↔ ( 𝐴 ≼ ω → ∪ 𝐴 ∈ 𝑆 ) ) )
13	12	rspcv	⊢ ( 𝐴 ∈ 𝒫 𝑆 → ( ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) → ( 𝐴 ≼ ω → ∪ 𝐴 ∈ 𝑆 ) ) )
14	1 7 8 13	syl3c	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω ) → ∪ 𝐴 ∈ 𝑆 )