Metamath Proof Explorer

Theorem salincl

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

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

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i F ) = ( E i^i F ) )
2 inss1 
 |-  ( E i^i F ) C_ E
3 2 a1i 
 |-  ( ( S e. SAlg /\ E e. S ) -> ( E i^i F ) C_ E )
4 elssuni 
 |-  ( E e. S -> E C_ U. S )
5 4 adantl 
 |-  ( ( S e. SAlg /\ E e. S ) -> E C_ U. S )
6 3 5 sstrd 
 |-  ( ( S e. SAlg /\ E e. S ) -> ( E i^i F ) C_ U. S )
7 dfss4 
 |-  ( ( E i^i F ) C_ U. S <-> ( U. S \ ( U. S \ ( E i^i F ) ) ) = ( E i^i F ) )
8 6 7 sylib 
 |-  ( ( S e. SAlg /\ E e. S ) -> ( U. S \ ( U. S \ ( E i^i F ) ) ) = ( E i^i F ) )
9 8 eqcomd 
 |-  ( ( S e. SAlg /\ E e. S ) -> ( E i^i F ) = ( U. S \ ( U. S \ ( E i^i F ) ) ) )
10 9 3adant3 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i F ) = ( U. S \ ( U. S \ ( E i^i F ) ) ) )
11 difindi 
 |-  ( U. S \ ( E i^i F ) ) = ( ( U. S \ E ) u. ( U. S \ F ) )
12 11 difeq2i 
 |-  ( U. S \ ( U. S \ ( E i^i F ) ) ) = ( U. S \ ( ( U. S \ E ) u. ( U. S \ F ) ) )
13 12 a1i 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( U. S \ ( U. S \ ( E i^i F ) ) ) = ( U. S \ ( ( U. S \ E ) u. ( U. S \ F ) ) ) )
14 1 10 13 3eqtrd 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i F ) = ( U. S \ ( ( U. S \ E ) u. ( U. S \ F ) ) ) )
15 simp1 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> S e. SAlg )
16 saldifcl 
 |-  ( ( S e. SAlg /\ E e. S ) -> ( U. S \ E ) e. S )
17 16 3adant3 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( U. S \ E ) e. S )
18 saldifcl 
 |-  ( ( S e. SAlg /\ F e. S ) -> ( U. S \ F ) e. S )
19 18 3adant2 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( U. S \ F ) e. S )
20 saluncl 
 |-  ( ( S e. SAlg /\ ( U. S \ E ) e. S /\ ( U. S \ F ) e. S ) -> ( ( U. S \ E ) u. ( U. S \ F ) ) e. S )
21 15 17 19 20 syl3anc 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( ( U. S \ E ) u. ( U. S \ F ) ) e. S )
22 saldifcl 
 |-  ( ( S e. SAlg /\ ( ( U. S \ E ) u. ( U. S \ F ) ) e. S ) -> ( U. S \ ( ( U. S \ E ) u. ( U. S \ F ) ) ) e. S )
23 15 21 22 syl2anc 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( U. S \ ( ( U. S \ E ) u. ( U. S \ F ) ) ) e. S )
24 14 23 eqeltrd 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i F ) e. S )