Metamath Proof Explorer

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 ⊢ S ∈ SAlg ∧ E ∈ S ∧ F ∈ S → E ∪ F ∈ S

Proof

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