Theorem saliinclf

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

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

Proof

Step	Hyp	Ref	Expression
1		saliinclf.1	$$⊢Ⅎk\phi$$
2		saliinclf.2	$$⊢\underset{\_}{Ⅎ}kS$$
3		saliinclf.3	$$⊢\underset{\_}{Ⅎ}kK$$
4		saliinclf.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
5		saliinclf.5	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
6		saliinclf.6	$$⊢\phi \to K\ne \varnothing$$
7		saliinclf.7	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
8		incom	$$⊢E\cap \bigcup S=\bigcup S\cap E$$
9		elssuni	$$⊢E\in S\to E\subseteq \bigcup S$$
10	7 9	syl	$$⊢\left(\phi \wedge k\in K\right)\to E\subseteq \bigcup S$$
11		df-ss	$$⊢E\subseteq \bigcup S\leftrightarrow E\cap \bigcup S=E$$
12	10 11	sylib	$$⊢\left(\phi \wedge k\in K\right)\to E\cap \bigcup S=E$$
13		dfin4	$$⊢\bigcup S\cap E=\bigcup S\setminus \left(\bigcup S\setminus E\right)$$
14	13	a1i	$$⊢\left(\phi \wedge k\in K\right)\to \bigcup S\cap E=\bigcup S\setminus \left(\bigcup S\setminus E\right)$$
15	8 12 14	3eqtr3a	$$⊢\left(\phi \wedge k\in K\right)\to E=\bigcup S\setminus \left(\bigcup S\setminus E\right)$$
16	1 15	iineq2d	$$⊢\phi \to \bigcap _{k\in K}E=\bigcap _{k\in K}\left(\bigcup S\setminus \left(\bigcup S\setminus E\right)\right)$$
17	2	nfuni	$$⊢\underset{\_}{Ⅎ}k\bigcup S$$
18	3 17	iindif2f	$$⊢K\ne \varnothing \to \bigcap _{k\in K}\left(\bigcup S\setminus \left(\bigcup S\setminus E\right)\right)=\bigcup S\setminus \bigcup _{k\in K}\left(\bigcup S\setminus E\right)$$
19	6 18	syl	$$⊢\phi \to \bigcap _{k\in K}\left(\bigcup S\setminus \left(\bigcup S\setminus E\right)\right)=\bigcup S\setminus \bigcup _{k\in K}\left(\bigcup S\setminus E\right)$$
20	16 19	eqtrd	$$⊢\phi \to \bigcap _{k\in K}E=\bigcup S\setminus \bigcup _{k\in K}\left(\bigcup S\setminus E\right)$$
21		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to \bigcup S\setminus E\in S$$
22	4 7 21	syl2an2r	$$⊢\left(\phi \wedge k\in K\right)\to \bigcup S\setminus E\in S$$
23	1 2 3 4 5 22	saliunclf	$$⊢\phi \to \bigcup _{k\in K}\left(\bigcup S\setminus E\right)\in S$$
24		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge \bigcup _{k\in K}\left(\bigcup S\setminus E\right)\in S\right)\to \bigcup S\setminus \bigcup _{k\in K}\left(\bigcup S\setminus E\right)\in S$$
25	4 23 24	syl2anc	$$⊢\phi \to \bigcup S\setminus \bigcup _{k\in K}\left(\bigcup S\setminus E\right)\in S$$
26	20 25	eqeltrd	$$⊢\phi \to \bigcap _{k\in K}E\in S$$