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 SAlg E S F S E F S

Proof

Step Hyp Ref Expression
1 eqidd S SAlg E S F S E F = E F
2 inss1 E F E
3 2 a1i S SAlg E S E F E
4 elssuni E S E S
5 4 adantl S SAlg E S E S
6 3 5 sstrd S SAlg E S E F S
7 dfss4 E F S S S E F = E F
8 6 7 sylib S SAlg E S S S E F = E F
9 8 eqcomd S SAlg E S E F = S S E F
10 9 3adant3 S SAlg E S F S E F = S S E F
11 difindi S E F = S E S F
12 11 difeq2i S S E F = S S E S F
13 12 a1i S SAlg E S F S S S E F = S S E S F
14 1 10 13 3eqtrd S SAlg E S F S E F = S S E S F
15 simp1 S SAlg E S F S S SAlg
16 saldifcl S SAlg E S S E S
17 16 3adant3 S SAlg E S F S S E S
18 saldifcl S SAlg F S S F S
19 18 3adant2 S SAlg E S F S S F S
20 saluncl S SAlg S E S S F S S E S F S
21 15 17 19 20 syl3anc S SAlg E S F S S E S F S
22 saldifcl S SAlg S E S F S S S E S F S
23 15 21 22 syl2anc S SAlg E S F S S S E S F S
24 14 23 eqeltrd S SAlg E S F S E F S