Theorem unelsiga

Description: A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016)

	Ref	Expression
Assertion	unelsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		uniprg	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
2	1	3adant1	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
3		isrnsigau	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
4	3	simprd	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
5	4	simp3d	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
6	5	3ad2ant1	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
7		prct	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ≼ ω )
8	7	3adant1	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ≼ ω )
9		prelpwi	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑆 )
10		breq1	⊢ ( 𝑥 = { 𝐴 , 𝐵 } → ( 𝑥 ≼ ω ↔ { 𝐴 , 𝐵 } ≼ ω ) )
11		unieq	⊢ ( 𝑥 = { 𝐴 , 𝐵 } → ∪ 𝑥 = ∪ { 𝐴 , 𝐵 } )
12	11	eleq1d	⊢ ( 𝑥 = { 𝐴 , 𝐵 } → ( ∪ 𝑥 ∈ 𝑆 ↔ ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) )
13	10 12	imbi12d	⊢ ( 𝑥 = { 𝐴 , 𝐵 } → ( ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ↔ ( { 𝐴 , 𝐵 } ≼ ω → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) ) )
14	13	rspcv	⊢ ( { 𝐴 , 𝐵 } ∈ 𝒫 𝑆 → ( ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) → ( { 𝐴 , 𝐵 } ≼ ω → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) ) )
15	9 14	syl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) → ( { 𝐴 , 𝐵 } ≼ ω → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) ) )
16	15	3adant1	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) → ( { 𝐴 , 𝐵 } ≼ ω → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) ) )
17	6 8 16	mp2d	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 )
18	2 17	eqeltrrd	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )