Metamath Proof Explorer

Theorem saliuncl

Description: SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses saliuncl.s ⊢ φ → S ∈ SAlg
saliuncl.kct ⊢ φ → K ≼ ω
saliuncl.b ⊢ φ ∧ k ∈ K → E ∈ S
Assertion saliuncl ⊢ φ → ⋃ k ∈ K E ∈ S

Proof

Step Hyp Ref Expression
1 saliuncl.s ⊢ φ → S ∈ SAlg
2 saliuncl.kct ⊢ φ → K ≼ ω
3 saliuncl.b ⊢ φ ∧ k ∈ K → E ∈ S
4 3 ralrimiva ⊢ φ → ∀ k ∈ K E ∈ S
5 dfiun3g ⊢ ∀ k ∈ K E ∈ S → ⋃ k ∈ K E = ⋃ ran ⁡ k ∈ K ⟼ E
6 4 5 syl ⊢ φ → ⋃ k ∈ K E = ⋃ ran ⁡ k ∈ K ⟼ E
7 eqid ⊢ k ∈ K ⟼ E = k ∈ K ⟼ E
8 7 rnmptss ⊢ ∀ k ∈ K E ∈ S → ran ⁡ k ∈ K ⟼ E ⊆ S
9 4 8 syl ⊢ φ → ran ⁡ k ∈ K ⟼ E ⊆ S
10 1 9 ssexd ⊢ φ → ran ⁡ k ∈ K ⟼ E ∈ V
11 elpwg ⊢ ran ⁡ k ∈ K ⟼ E ∈ V → ran ⁡ k ∈ K ⟼ E ∈ 𝒫 S ↔ ran ⁡ k ∈ K ⟼ E ⊆ S
12 10 11 syl ⊢ φ → ran ⁡ k ∈ K ⟼ E ∈ 𝒫 S ↔ ran ⁡ k ∈ K ⟼ E ⊆ S
13 9 12 mpbird ⊢ φ → ran ⁡ k ∈ K ⟼ E ∈ 𝒫 S
14 1stcrestlem ⊢ K ≼ ω → ran ⁡ k ∈ K ⟼ E ≼ ω
15 2 14 syl ⊢ φ → ran ⁡ k ∈ K ⟼ E ≼ ω
16 1 13 15 salunicl ⊢ φ → ⋃ ran ⁡ k ∈ K ⟼ E ∈ S
17 6 16 eqeltrd ⊢ φ → ⋃ k ∈ K E ∈ S