Theorem sigaclci

Description: A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016)

	Ref	Expression
Assertion	sigaclci	$$⊢\left(\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\wedge \left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\right)\to \bigcap A\in S$$

Proof

Step	Hyp	Ref	Expression
1		isrnsigau	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(S\subseteq 𝒫\bigcup S\wedge \left(\bigcup S\in S\wedge \forall x\in S\bigcup S\setminus x\in S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)\right)$$
2	1	simprd	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(\bigcup S\in S\wedge \forall x\in S\bigcup S\setminus x\in S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)$$
3	2	simp2d	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \forall x\in S\bigcup S\setminus x\in S$$
4	3	adantr	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \forall x\in S\bigcup S\setminus x\in S$$
5		elpwi	$$⊢A\in 𝒫S\to A\subseteq S$$
6		ssrexv	$$⊢A\subseteq S\to \left(\exists z\in Ay=\bigcup S\setminus z\to \exists z\in Sy=\bigcup S\setminus z\right)$$
7	5 6	syl	$$⊢A\in 𝒫S\to \left(\exists z\in Ay=\bigcup S\setminus z\to \exists z\in Sy=\bigcup S\setminus z\right)$$
8	7	ss2abdv	$$⊢A\in 𝒫S\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\subseteq \left\{y|\exists z\in Sy=\bigcup S\setminus z\right\}$$
9		isrnsigau	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(S\subseteq 𝒫\bigcup S\wedge \left(\bigcup S\in S\wedge \forall z\in S\bigcup S\setminus z\in S\wedge \forall z\in 𝒫S\left(z\preccurlyeq \mathrm{\omega }\to \bigcup z\in S\right)\right)\right)$$
10	9	simprd	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(\bigcup S\in S\wedge \forall z\in S\bigcup S\setminus z\in S\wedge \forall z\in 𝒫S\left(z\preccurlyeq \mathrm{\omega }\to \bigcup z\in S\right)\right)$$
11	10	simp2d	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \forall z\in S\bigcup S\setminus z\in S$$
12		uniiunlem	$$⊢\forall z\in S\bigcup S\setminus z\in S\to \left(\forall z\in S\bigcup S\setminus z\in S\leftrightarrow \left\{y|\exists z\in Sy=\bigcup S\setminus z\right\}\subseteq S\right)$$
13	11 12	syl	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(\forall z\in S\bigcup S\setminus z\in S\leftrightarrow \left\{y|\exists z\in Sy=\bigcup S\setminus z\right\}\subseteq S\right)$$
14	11 13	mpbid	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left\{y|\exists z\in Sy=\bigcup S\setminus z\right\}\subseteq S$$
15	8 14	sylan9ssr	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\subseteq S$$
16		abrexexg	$$⊢A\in 𝒫S\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in \mathrm{V}$$
17		elpwg	$$⊢\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in \mathrm{V}\to \left(\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in 𝒫S\leftrightarrow \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\subseteq S\right)$$
18	16 17	syl	$$⊢A\in 𝒫S\to \left(\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in 𝒫S\leftrightarrow \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\subseteq S\right)$$
19	18	adantl	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in 𝒫S\leftrightarrow \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\subseteq S\right)$$
20	15 19	mpbird	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in 𝒫S$$
21	2	simp3d	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)$$
22	21	adantr	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)$$
23	20 22	jca	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in 𝒫S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)$$
24		abrexdom2jm	$$⊢A\in 𝒫S\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq A$$
25		domtr	$$⊢\left(\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq A\wedge A\preccurlyeq \mathrm{\omega }\right)\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq \mathrm{\omega }$$
26	24 25	sylan	$$⊢\left(A\in 𝒫S\wedge A\preccurlyeq \mathrm{\omega }\right)\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq \mathrm{\omega }$$
27	26	ex	$$⊢A\in 𝒫S\to \left(A\preccurlyeq \mathrm{\omega }\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq \mathrm{\omega }\right)$$
28	27	adantl	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(A\preccurlyeq \mathrm{\omega }\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq \mathrm{\omega }\right)$$
29		breq1	$$⊢x=\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\to \left(x\preccurlyeq \mathrm{\omega }\leftrightarrow \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq \mathrm{\omega }\right)$$
30		unieq	$$⊢x=\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\to \bigcup x=\bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}$$
31	30	eleq1d	$$⊢x=\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\to \left(\bigcup x\in S\leftrightarrow \bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in S\right)$$
32	29 31	imbi12d	$$⊢x=\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\to \left(\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\leftrightarrow \left(\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq \mathrm{\omega }\to \bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in S\right)\right)$$
33	32	rspcva	$$⊢\left(\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in 𝒫S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)\to \left(\left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq \mathrm{\omega }\to \bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in S\right)$$
34	23 28 33	sylsyld	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(A\preccurlyeq \mathrm{\omega }\to \bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in S\right)$$
35	5	adantl	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to A\subseteq S$$
36	11	adantr	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \forall z\in S\bigcup S\setminus z\in S$$
37		ssralv	$$⊢A\subseteq S\to \left(\forall z\in S\bigcup S\setminus z\in S\to \forall z\in A\bigcup S\setminus z\in S\right)$$
38	35 36 37	sylc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \forall z\in A\bigcup S\setminus z\in S$$
39		dfiun2g	$$⊢\forall z\in A\bigcup S\setminus z\in S\to \bigcup _{z\in A}\left(\bigcup S\setminus z\right)=\bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}$$
40		eleq1	$$⊢\bigcup _{z\in A}\left(\bigcup S\setminus z\right)=\bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\to \left(\bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\leftrightarrow \bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in S\right)$$
41	38 39 40	3syl	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(\bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\leftrightarrow \bigcup \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\in S\right)$$
42	34 41	sylibrd	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(A\preccurlyeq \mathrm{\omega }\to \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\right)$$
43		difeq2	$$⊢x=\bigcup _{z\in A}\left(\bigcup S\setminus z\right)\to \bigcup S\setminus x=\bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)$$
44	43	eleq1d	$$⊢x=\bigcup _{z\in A}\left(\bigcup S\setminus z\right)\to \left(\bigcup S\setminus x\in S\leftrightarrow \bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\right)$$
45	44	rspccv	$$⊢\forall x\in S\bigcup S\setminus x\in S\to \left(\bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\to \bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\right)$$
46	4 42 45	sylsyld	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(A\preccurlyeq \mathrm{\omega }\to \bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\right)$$
47	46	adantrd	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to \bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\right)$$
48	47	imp	$$⊢\left(\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\wedge \left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\right)\to \bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S$$
49		simpr	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to A\in 𝒫S$$
50		pwuni	$$⊢S\subseteq 𝒫\bigcup S$$
51	5 50	sstrdi	$$⊢A\in 𝒫S\to A\subseteq 𝒫\bigcup S$$
52		iundifdifd	$$⊢A\subseteq 𝒫\bigcup S\to \left(A\ne \varnothing \to \bigcap A=\bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\right)$$
53	49 51 52	3syl	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(A\ne \varnothing \to \bigcap A=\bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\right)$$
54	53	adantld	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to \bigcap A=\bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\right)$$
55		eleq1	$$⊢\bigcap A=\bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\to \left(\bigcap A\in S\leftrightarrow \bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\right)$$
56	54 55	syl6	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to \left(\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to \left(\bigcap A\in S\leftrightarrow \bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\right)\right)$$
57	56	imp	$$⊢\left(\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\wedge \left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\right)\to \left(\bigcap A\in S\leftrightarrow \bigcup S\setminus \bigcup _{z\in A}\left(\bigcup S\setminus z\right)\in S\right)$$
58	48 57	mpbird	$$⊢\left(\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\wedge \left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\right)\to \bigcap A\in S$$