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 ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) = ( 𝐸 ∩ 𝐹 ) )
2 inss1 ⊢ ( 𝐸 ∩ 𝐹 ) ⊆ 𝐸
3 2 a1i ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) ⊆ 𝐸 )
4 elssuni ⊢ ( 𝐸 ∈ 𝑆 → 𝐸 ⊆ ∪ 𝑆 )
5 4 adantl ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → 𝐸 ⊆ ∪ 𝑆 )
6 3 5 sstrd ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) ⊆ ∪ 𝑆 )
7 dfss4 ⊢ ( ( 𝐸 ∩ 𝐹 ) ⊆ ∪ 𝑆 ↔ ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ ( 𝐸 ∩ 𝐹 ) ) ) = ( 𝐸 ∩ 𝐹 ) )
8 6 7 sylib ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ ( 𝐸 ∩ 𝐹 ) ) ) = ( 𝐸 ∩ 𝐹 ) )
9 8 eqcomd ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) = ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ ( 𝐸 ∩ 𝐹 ) ) ) )
10 9 3adant3 ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) = ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ ( 𝐸 ∩ 𝐹 ) ) ) )
11 difindi ⊢ ( ∪ 𝑆 ∖ ( 𝐸 ∩ 𝐹 ) ) = ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) )
12 11 difeq2i ⊢ ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ ( 𝐸 ∩ 𝐹 ) ) ) = ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) ) )
13 12 a1i ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ ( 𝐸 ∩ 𝐹 ) ) ) = ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) ) ) )
14 1 10 13 3eqtrd ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) = ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) ) ) )
15 simp1 ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → 𝑆 ∈ SAlg )
16 saldifcl ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )
17 16 3adant3 ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )
18 saldifcl ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐹 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐹 ) ∈ 𝑆 )
19 18 3adant2 ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐹 ) ∈ 𝑆 )
20 saluncl ⊢ ( ( 𝑆 ∈ SAlg ∧ ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 ∧ ( ∪ 𝑆 ∖ 𝐹 ) ∈ 𝑆 ) → ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) ) ∈ 𝑆 )
21 15 17 19 20 syl3anc ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) ) ∈ 𝑆 )
22 saldifcl ⊢ ( ( 𝑆 ∈ SAlg ∧ ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) ) ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) ) ) ∈ 𝑆 )
23 15 21 22 syl2anc ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐸 ) ∪ ( ∪ 𝑆 ∖ 𝐹 ) ) ) ∈ 𝑆 )
24 14 23 eqeltrd ⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∩ 𝐹 ) ∈ 𝑆 )