Theorem saldifcl2

Description: The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	saldifcl2	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E \ F ) e. S )

Proof

Step	Hyp	Ref	Expression
1		indif2	|- ( E i^i ( U. S \ F ) ) = ( ( E i^i U. S ) \ F )
2	1	a1i	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i ( U. S \ F ) ) = ( ( E i^i U. S ) \ F ) )
3		elssuni	|- ( E e. S -> E C_ U. S )
4		dfss2	|- ( E C_ U. S <-> ( E i^i U. S ) = E )
5	3 4	sylib	|- ( E e. S -> ( E i^i U. S ) = E )
6	5	difeq1d	|- ( E e. S -> ( ( E i^i U. S ) \ F ) = ( E \ F ) )
7	6	3ad2ant2	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( ( E i^i U. S ) \ F ) = ( E \ F ) )
8	2 7	eqtr2d	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E \ F ) = ( E i^i ( U. S \ F ) ) )
9		simp1	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> S e. SAlg )
10		simp2	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> E e. S )
11		saldifcl	|- ( ( S e. SAlg /\ F e. S ) -> ( U. S \ F ) e. S )
12	11	3adant2	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( U. S \ F ) e. S )
13		salincl	|- ( ( S e. SAlg /\ E e. S /\ ( U. S \ F ) e. S ) -> ( E i^i ( U. S \ F ) ) e. S )
14	9 10 12 13	syl3anc	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i ( U. S \ F ) ) e. S )
15	8 14	eqeltrd	|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E \ F ) e. S )