Metamath Proof Explorer


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 df-ss
 |-  ( 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 )