Theorem difelsiga

Description: A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016)

	Ref	Expression
Assertion	difelsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\setminus B\in S$$

Proof

Step	Hyp	Ref	Expression
1		simp2	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\in S$$
2		elssuni	$$⊢A\in S\to A\subseteq \bigcup S$$
3		difin2	$$⊢A\subseteq \bigcup S\to A\setminus B=\left(\bigcup S\setminus B\right)\cap A$$
4	1 2 3	3syl	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\setminus B=\left(\bigcup S\setminus B\right)\cap A$$
5		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)$$
6	5	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)$$
7	6	simp2d	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \forall x\in S\bigcup S\setminus x\in S$$
8		difeq2	$$⊢x=B\to \bigcup S\setminus x=\bigcup S\setminus B$$
9	8	eleq1d	$$⊢x=B\to \left(\bigcup S\setminus x\in S\leftrightarrow \bigcup S\setminus B\in S\right)$$
10	9	rspccva	$$⊢\left(\forall x\in S\bigcup S\setminus x\in S\wedge B\in S\right)\to \bigcup S\setminus B\in S$$
11	7 10	sylan	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge B\in S\right)\to \bigcup S\setminus B\in S$$
12	11	3adant2	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \bigcup S\setminus B\in S$$
13		intprg	$$⊢\left(\bigcup S\setminus B\in S\wedge A\in S\right)\to \bigcap \left\{\bigcup S\setminus B,A\right\}=\left(\bigcup S\setminus B\right)\cap A$$
14	12 1 13	syl2anc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \bigcap \left\{\bigcup S\setminus B,A\right\}=\left(\bigcup S\setminus B\right)\cap A$$
15	4 14	eqtr4d	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\setminus B=\bigcap \left\{\bigcup S\setminus B,A\right\}$$
16		simp1	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
17		prssi	$$⊢\left(\bigcup S\setminus B\in S\wedge A\in S\right)\to \left\{\bigcup S\setminus B,A\right\}\subseteq S$$
18	12 1 17	syl2anc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \left\{\bigcup S\setminus B,A\right\}\subseteq S$$
19		prex	$$⊢\left\{\bigcup S\setminus B,A\right\}\in \mathrm{V}$$
20	19	elpw	$$⊢\left\{\bigcup S\setminus B,A\right\}\in 𝒫S\leftrightarrow \left\{\bigcup S\setminus B,A\right\}\subseteq S$$
21	18 20	sylibr	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \left\{\bigcup S\setminus B,A\right\}\in 𝒫S$$
22		prct	$$⊢\left(\bigcup S\setminus B\in S\wedge A\in S\right)\to \left\{\bigcup S\setminus B,A\right\}\preccurlyeq \mathrm{\omega }$$
23	12 1 22	syl2anc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \left\{\bigcup S\setminus B,A\right\}\preccurlyeq \mathrm{\omega }$$
24		prnzg	$$⊢\bigcup S\setminus B\in S\to \left\{\bigcup S\setminus B,A\right\}\ne \varnothing$$
25	12 24	syl	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \left\{\bigcup S\setminus B,A\right\}\ne \varnothing$$
26		sigaclci	$$⊢\left(\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \left\{\bigcup S\setminus B,A\right\}\in 𝒫S\right)\wedge \left(\left\{\bigcup S\setminus B,A\right\}\preccurlyeq \mathrm{\omega }\wedge \left\{\bigcup S\setminus B,A\right\}\ne \varnothing \right)\right)\to \bigcap \left\{\bigcup S\setminus B,A\right\}\in S$$
27	16 21 23 25 26	syl22anc	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to \bigcap \left\{\bigcup S\setminus B,A\right\}\in S$$
28	15 27	eqeltrd	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\wedge B\in S\right)\to A\setminus B\in S$$