Theorem saliuncl

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

	Ref	Expression
Hypotheses	saliuncl.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	saliuncl.kct	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
	saliuncl.b	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
Assertion	saliuncl	$$⊢\phi \to \bigcup _{k\in K}E\in S$$

Proof

Step	Hyp	Ref	Expression
1		saliuncl.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		saliuncl.kct	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
3		saliuncl.b	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
4		nfv	$$⊢Ⅎk\phi$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}kS$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}kK$$
7	4 5 6 1 2 3	saliunclf	$$⊢\phi \to \bigcup _{k\in K}E\in S$$