Theorem salunicl

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

	Ref	Expression
Hypotheses	salunicl.s	|- ( ph -> S e. SAlg )
	salunicl.t	|- ( ph -> T e. ~P S )
	salunicl.tct	|- ( ph -> T ~<_ _om )
Assertion	salunicl	|- ( ph -> U. T e. S )

Proof

Step	Hyp	Ref	Expression
1		salunicl.s	|- ( ph -> S e. SAlg )
2		salunicl.t	|- ( ph -> T e. ~P S )
3		salunicl.tct	|- ( ph -> T ~<_ _om )
4		breq1	|- ( y = T -> ( y ~<_ _om <-> T ~<_ _om ) )
5		unieq	|- ( y = T -> U. y = U. T )
6	5	eleq1d	|- ( y = T -> ( U. y e. S <-> U. T e. S ) )
7	4 6	imbi12d	|- ( y = T -> ( ( y ~<_ _om -> U. y e. S ) <-> ( T ~<_ _om -> U. T e. S ) ) )
8		issal	|- ( S e. SAlg -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
9	1 8	syl	|- ( ph -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
10	1 9	mpbid	|- ( ph -> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) )
11	10	simp3d	|- ( ph -> A. y e. ~P S ( y ~<_ _om -> U. y e. S ) )
12	7 11 2	rspcdva	|- ( ph -> ( T ~<_ _om -> U. T e. S ) )
13	3 12	mpd	|- ( ph -> U. T e. S )