Theorem salunicl

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

	Ref	Expression
Hypotheses	salunicl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	salunicl.t	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝑆 )
	salunicl.tct	⊢ ( 𝜑 → 𝑇 ≼ ω )
Assertion	salunicl	⊢ ( 𝜑 → ∪ 𝑇 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		salunicl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		salunicl.t	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝑆 )
3		salunicl.tct	⊢ ( 𝜑 → 𝑇 ≼ ω )
4		breq1	⊢ ( 𝑦 = 𝑇 → ( 𝑦 ≼ ω ↔ 𝑇 ≼ ω ) )
5		unieq	⊢ ( 𝑦 = 𝑇 → ∪ 𝑦 = ∪ 𝑇 )
6	5	eleq1d	⊢ ( 𝑦 = 𝑇 → ( ∪ 𝑦 ∈ 𝑆 ↔ ∪ 𝑇 ∈ 𝑆 ) )
7	4 6	imbi12d	⊢ ( 𝑦 = 𝑇 → ( ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ↔ ( 𝑇 ≼ ω → ∪ 𝑇 ∈ 𝑆 ) ) )
8		issal	⊢ ( 𝑆 ∈ SAlg → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
9	1 8	syl	⊢ ( 𝜑 → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
10	1 9	mpbid	⊢ ( 𝜑 → ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) )
11	10	simp3d	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) )
12	7 11 2	rspcdva	⊢ ( 𝜑 → ( 𝑇 ≼ ω → ∪ 𝑇 ∈ 𝑆 ) )
13	3 12	mpd	⊢ ( 𝜑 → ∪ 𝑇 ∈ 𝑆 )