Theorem saliunclf

Description: SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	saliunclf.1	$$⊢Ⅎk\phi$$
	saliunclf.2	$$⊢\underset{\_}{Ⅎ}kS$$
	saliunclf.3	$$⊢\underset{\_}{Ⅎ}kK$$
	saliunclf.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
	saliunclf.5	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
	saliunclf.6	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
Assertion	saliunclf	$$⊢\phi \to \bigcup _{k\in K}E\in S$$

Proof

Step	Hyp	Ref	Expression
1		saliunclf.1	$$⊢Ⅎk\phi$$
2		saliunclf.2	$$⊢\underset{\_}{Ⅎ}kS$$
3		saliunclf.3	$$⊢\underset{\_}{Ⅎ}kK$$
4		saliunclf.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
5		saliunclf.5	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
6		saliunclf.6	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
7	1 6	ralrimia	$$⊢\phi \to \forall k\in KE\in S$$
8		dfiun3g	$$⊢\forall k\in KE\in S\to \bigcup _{k\in K}E=\bigcup \mathrm{ran}\left(k\in K⟼E\right)$$
9	7 8	syl	$$⊢\phi \to \bigcup _{k\in K}E=\bigcup \mathrm{ran}\left(k\in K⟼E\right)$$
10		eqid	$$⊢\left(k\in K⟼E\right)=\left(k\in K⟼E\right)$$
11	1 3 2 10 6	rnmptssdff	$$⊢\phi \to \mathrm{ran}\left(k\in K⟼E\right)\subseteq S$$
12	4 11	sselpwd	$$⊢\phi \to \mathrm{ran}\left(k\in K⟼E\right)\in 𝒫S$$
13	3	rn1st	$$⊢K\preccurlyeq \mathrm{\omega }\to \mathrm{ran}\left(k\in K⟼E\right)\preccurlyeq \mathrm{\omega }$$
14	5 13	syl	$$⊢\phi \to \mathrm{ran}\left(k\in K⟼E\right)\preccurlyeq \mathrm{\omega }$$
15	4 12 14	salunicl	$$⊢\phi \to \bigcup \mathrm{ran}\left(k\in K⟼E\right)\in S$$
16	9 15	eqeltrd	$$⊢\phi \to \bigcup _{k\in K}E\in S$$