Theorem sigaclci

Description: A sigma-algebra is closed under countable intersections. Deduction version. The proof uses abrexct rather than abrexdom2jm , and so does not require ax-ac . (Contributed by Thierry Arnoux, 19-Sep-2016) (Revised by Vincent Gonzalez, 19-Aug-2026)

	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		abrexct	$$⊢A\preccurlyeq \mathrm{\omega }\to \left\{y|\exists z\in Ay=\bigcup S\setminus z\right\}\preccurlyeq \mathrm{\omega }$$
25	24	adantl	$$⊢\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 }$$
26	25	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)$$
27	26	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)$$
28		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)$$
29		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\}$$
30	29	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)$$
31	28 30	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)$$
32	31	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)$$
33	23 27 32	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)$$
34	5	adantl	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to A\subseteq S$$
35	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$$
36		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)$$
37	34 35 36	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$$
38		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\}$$
39		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)$$
40	37 38 39	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)$$
41	33 40	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)$$
42		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)$$
43	42	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)$$
44	43	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)$$
45	4 41 44	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)$$
46	45	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)$$
47	46	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$$
48		simpr	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in 𝒫S\right)\to A\in 𝒫S$$
49		pwuni	$$⊢S\subseteq 𝒫\bigcup S$$
50	5 49	sstrdi	$$⊢A\in 𝒫S\to A\subseteq 𝒫\bigcup S$$
51		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)$$
52	48 50 51	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)$$
53	52	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)$$
54		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)$$
55	53 54	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)$$
56	55	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)$$
57	47 56	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$$