Metamath Proof Explorer

Theorem saliunclf

Description: SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypotheses saliunclf.1 ⊢ Ⅎ k φ
saliunclf.2 ⊢ Ⅎ _ k S
saliunclf.3 ⊢ Ⅎ _ k K
saliunclf.4 ⊢ φ → S ∈ SAlg
saliunclf.5 ⊢ φ → K ≼ ω
saliunclf.6 ⊢ φ ∧ k ∈ K → E ∈ S
Assertion saliunclf ⊢ φ → ⋃ k ∈ K E ∈ S

Proof

Step Hyp Ref Expression
1 saliunclf.1 ⊢ Ⅎ k φ
2 saliunclf.2 ⊢ Ⅎ _ k S
3 saliunclf.3 ⊢ Ⅎ _ k K
4 saliunclf.4 ⊢ φ → S ∈ SAlg
5 saliunclf.5 ⊢ φ → K ≼ ω
6 saliunclf.6 ⊢ φ ∧ k ∈ K → E ∈ S
7 1 6 ralrimia ⊢ φ → ∀ k ∈ K E ∈ S
8 dfiun3g ⊢ ∀ k ∈ K E ∈ S → ⋃ k ∈ K E = ⋃ ran ⁡ k ∈ K ⟼ E
9 7 8 syl ⊢ φ → ⋃ k ∈ K E = ⋃ ran ⁡ k ∈ K ⟼ E
10 eqid ⊢ k ∈ K ⟼ E = k ∈ K ⟼ E
11 1 3 2 10 6 rnmptssdff ⊢ φ → ran ⁡ k ∈ K ⟼ E ⊆ S
12 4 11 sselpwd ⊢ φ → ran ⁡ k ∈ K ⟼ E ∈ 𝒫 S
13 3 rn1st ⊢ K ≼ ω → ran ⁡ k ∈ K ⟼ E ≼ ω
14 5 13 syl ⊢ φ → ran ⁡ k ∈ K ⟼ E ≼ ω
15 4 12 14 salunicl ⊢ φ → ⋃ ran ⁡ k ∈ K ⟼ E ∈ S
16 9 15 eqeltrd ⊢ φ → ⋃ k ∈ K E ∈ S