Theorem salunicl

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

	Ref	Expression
Hypotheses	salunicl.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	salunicl.t	$$⊢\phi \to T\in 𝒫S$$
	salunicl.tct	$$⊢\phi \to T\preccurlyeq \mathrm{\omega }$$
Assertion	salunicl	$$⊢\phi \to \bigcup T\in S$$

Proof

Step	Hyp	Ref	Expression
1		salunicl.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		salunicl.t	$$⊢\phi \to T\in 𝒫S$$
3		salunicl.tct	$$⊢\phi \to T\preccurlyeq \mathrm{\omega }$$
4		breq1	$$⊢y=T\to \left(y\preccurlyeq \mathrm{\omega }\leftrightarrow T\preccurlyeq \mathrm{\omega }\right)$$
5		unieq	$$⊢y=T\to \bigcup y=\bigcup T$$
6	5	eleq1d	$$⊢y=T\to \left(\bigcup y\in S\leftrightarrow \bigcup T\in S\right)$$
7	4 6	imbi12d	$$⊢y=T\to \left(\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\leftrightarrow \left(T\preccurlyeq \mathrm{\omega }\to \bigcup T\in S\right)\right)$$
8		issal	$$⊢S\in \mathrm{SAlg}\to \left(S\in \mathrm{SAlg}\leftrightarrow \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)\right)$$
9	1 8	syl	$$⊢\phi \to \left(S\in \mathrm{SAlg}\leftrightarrow \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)\right)$$
10	1 9	mpbid	$$⊢\phi \to \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)$$
11	10	simp3d	$$⊢\phi \to \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)$$
12	7 11 2	rspcdva	$$⊢\phi \to \left(T\preccurlyeq \mathrm{\omega }\to \bigcup T\in S\right)$$
13	3 12	mpd	$$⊢\phi \to \bigcup T\in S$$