Theorem saliincl

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

	Ref	Expression
Hypotheses	saliincl.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	saliincl.kct	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
	saliincl.kn0	$$⊢\phi \to K\ne \varnothing$$
	saliincl.e	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
Assertion	saliincl	$$⊢\phi \to \bigcap _{k\in K}E\in S$$

Proof

Step	Hyp	Ref	Expression
1		saliincl.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		saliincl.kct	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
3		saliincl.kn0	$$⊢\phi \to K\ne \varnothing$$
4		saliincl.e	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
5		elssuni	$$⊢E\in S\to E\subseteq \bigcup S$$
6	4 5	syl	$$⊢\left(\phi \wedge k\in K\right)\to E\subseteq \bigcup S$$
7		df-ss	$$⊢E\subseteq \bigcup S\leftrightarrow E\cap \bigcup S=E$$
8	6 7	sylib	$$⊢\left(\phi \wedge k\in K\right)\to E\cap \bigcup S=E$$
9	8	eqcomd	$$⊢\left(\phi \wedge k\in K\right)\to E=E\cap \bigcup S$$
10		incom	$$⊢E\cap \bigcup S=\bigcup S\cap E$$
11	10	a1i	$$⊢\left(\phi \wedge k\in K\right)\to E\cap \bigcup S=\bigcup S\cap E$$
12		dfin4	$$⊢\bigcup S\cap E=\bigcup S\setminus \left(\bigcup S\setminus E\right)$$
13	12	a1i	$$⊢\left(\phi \wedge k\in K\right)\to \bigcup S\cap E=\bigcup S\setminus \left(\bigcup S\setminus E\right)$$
14	9 11 13	3eqtrd	$$⊢\left(\phi \wedge k\in K\right)\to E=\bigcup S\setminus \left(\bigcup S\setminus E\right)$$
15	14	iineq2dv	$$⊢\phi \to \bigcap _{k\in K}E=\bigcap _{k\in K}\left(\bigcup S\setminus \left(\bigcup S\setminus E\right)\right)$$
16		iindif2	$$⊢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)$$
17	3 16	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)$$
18	15 17	eqtrd	$$⊢\phi \to \bigcap _{k\in K}E=\bigcup S\setminus \bigcup _{k\in K}\left(\bigcup S\setminus E\right)$$
19	1	adantr	$$⊢\left(\phi \wedge k\in K\right)\to S\in \mathrm{SAlg}$$
20		saldifcl	$$⊢\left(S\in \mathrm{SAlg}\wedge E\in S\right)\to \bigcup S\setminus E\in S$$
21	19 4 20	syl2anc	$$⊢\left(\phi \wedge k\in K\right)\to \bigcup S\setminus E\in S$$
22	1 2 21	saliuncl	$$⊢\phi \to \bigcup _{k\in K}\left(\bigcup S\setminus E\right)\in S$$
23		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$$
24	1 22 23	syl2anc	$$⊢\phi \to \bigcup S\setminus \bigcup _{k\in K}\left(\bigcup S\setminus E\right)\in S$$
25	18 24	eqeltrd	$$⊢\phi \to \bigcap _{k\in K}E\in S$$