Theorem saluncl

Description: The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	saluncl	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∪ 𝐹 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		uniprg	⊢ ( ( 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ∪ { 𝐸 , 𝐹 } = ( 𝐸 ∪ 𝐹 ) )
2	1	eqcomd	⊢ ( ( 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∪ 𝐹 ) = ∪ { 𝐸 , 𝐹 } )
3	2	3adant1	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∪ 𝐹 ) = ∪ { 𝐸 , 𝐹 } )
4		prfi	⊢ { 𝐸 , 𝐹 } ∈ Fin
5		isfinite	⊢ ( { 𝐸 , 𝐹 } ∈ Fin ↔ { 𝐸 , 𝐹 } ≺ ω )
6	5	biimpi	⊢ ( { 𝐸 , 𝐹 } ∈ Fin → { 𝐸 , 𝐹 } ≺ ω )
7		sdomdom	⊢ ( { 𝐸 , 𝐹 } ≺ ω → { 𝐸 , 𝐹 } ≼ ω )
8	6 7	syl	⊢ ( { 𝐸 , 𝐹 } ∈ Fin → { 𝐸 , 𝐹 } ≼ ω )
9	4 8	ax-mp	⊢ { 𝐸 , 𝐹 } ≼ ω
10	9	a1i	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → { 𝐸 , 𝐹 } ≼ ω )
11		prelpwi	⊢ ( ( 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → { 𝐸 , 𝐹 } ∈ 𝒫 𝑆 )
12	11	3adant1	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → { 𝐸 , 𝐹 } ∈ 𝒫 𝑆 )
13		issal	⊢ ( 𝑆 ∈ SAlg → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
14	13	ibi	⊢ ( 𝑆 ∈ SAlg → ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) )
15	14	simp3d	⊢ ( 𝑆 ∈ SAlg → ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) )
16	15	3ad2ant1	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) )
17		breq1	⊢ ( 𝑦 = { 𝐸 , 𝐹 } → ( 𝑦 ≼ ω ↔ { 𝐸 , 𝐹 } ≼ ω ) )
18		unieq	⊢ ( 𝑦 = { 𝐸 , 𝐹 } → ∪ 𝑦 = ∪ { 𝐸 , 𝐹 } )
19	18	eleq1d	⊢ ( 𝑦 = { 𝐸 , 𝐹 } → ( ∪ 𝑦 ∈ 𝑆 ↔ ∪ { 𝐸 , 𝐹 } ∈ 𝑆 ) )
20	17 19	imbi12d	⊢ ( 𝑦 = { 𝐸 , 𝐹 } → ( ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ↔ ( { 𝐸 , 𝐹 } ≼ ω → ∪ { 𝐸 , 𝐹 } ∈ 𝑆 ) ) )
21	20	rspcva	⊢ ( ( { 𝐸 , 𝐹 } ∈ 𝒫 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) → ( { 𝐸 , 𝐹 } ≼ ω → ∪ { 𝐸 , 𝐹 } ∈ 𝑆 ) )
22	12 16 21	syl2anc	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( { 𝐸 , 𝐹 } ≼ ω → ∪ { 𝐸 , 𝐹 } ∈ 𝑆 ) )
23	10 22	mpd	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ∪ { 𝐸 , 𝐹 } ∈ 𝑆 )
24	3 23	eqeltrd	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∪ 𝐹 ) ∈ 𝑆 )