Theorem saliuncl

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

	Ref	Expression
Hypotheses	saliuncl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	saliuncl.kct	⊢ ( 𝜑 → 𝐾 ≼ ω )
	saliuncl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
Assertion	saliuncl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		saliuncl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		saliuncl.kct	⊢ ( 𝜑 → 𝐾 ≼ ω )
3		saliuncl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
4	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )
5		dfiun3g	⊢ ( ∀ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 → ∪ 𝑘 ∈ 𝐾 𝐸 = ∪ ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) )
6	4 5	syl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 = ∪ ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) )
7		eqid	⊢ ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) = ( 𝑘 ∈ 𝐾 ↦ 𝐸 )
8	7	rnmptss	⊢ ( ∀ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ⊆ 𝑆 )
9	4 8	syl	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ⊆ 𝑆 )
10	1 9	ssexd	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ∈ V )
11		elpwg	⊢ ( ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ∈ V → ( ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ∈ 𝒫 𝑆 ↔ ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ⊆ 𝑆 ) )
12	10 11	syl	⊢ ( 𝜑 → ( ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ∈ 𝒫 𝑆 ↔ ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ⊆ 𝑆 ) )
13	9 12	mpbird	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ∈ 𝒫 𝑆 )
14		1stcrestlem	⊢ ( 𝐾 ≼ ω → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ≼ ω )
15	2 14	syl	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ≼ ω )
16	1 13 15	salunicl	⊢ ( 𝜑 → ∪ ran ( 𝑘 ∈ 𝐾 ↦ 𝐸 ) ∈ 𝑆 )
17	6 16	eqeltrd	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )