Theorem saliunclf

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

	Ref	Expression
Hypotheses	saliunclf.1	⊢ Ⅎ 𝑘 𝜑
	saliunclf.2	⊢ Ⅎ 𝑘 𝑆
	saliunclf.3	⊢ Ⅎ 𝑘 𝐾
	saliunclf.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	saliunclf.5	⊢ ( 𝜑 → 𝐾 ≼ ω )
	saliunclf.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
Assertion	saliunclf	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		saliunclf.1	⊢ Ⅎ 𝑘 𝜑
2		saliunclf.2	⊢ Ⅎ 𝑘 𝑆
3		saliunclf.3	⊢ Ⅎ 𝑘 𝐾
4		saliunclf.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
5		saliunclf.5	⊢ ( 𝜑 → 𝐾 ≼ ω )
6		saliunclf.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
7	1 6	ralrimia	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )
8		dfiun3g	⊢ ( ∀ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 → ∪ 𝑘 ∈ 𝐾 𝐸 = ∪ ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) )
9	7 8	syl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 = ∪ ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) )
10		eqid	⊢ ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) = ( 𝑘 ∈ 𝐾 ↦ 𝐸 )
11	1 3 2 10 6	rnmptssdff	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ⊆ 𝑆 )
12	4 11	sselpwd	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ∈ 𝒫 𝑆 )
13	3	rn1st	⊢ ( 𝐾 ≼ ω → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ≼ ω )
14	5 13	syl	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ≼ ω )
15	4 12 14	salunicl	⊢ ( 𝜑 → ∪ ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ∈ 𝑆 )
16	9 15	eqeltrd	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )