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

Proof

Step	Hyp	Ref	Expression
1		indif2	⊢ ( 𝐸 ∩ ( ∪ 𝑆 ∖ 𝐹 ) ) = ( ( 𝐸 ∩ ∪ 𝑆 ) ∖ 𝐹 )
2	1	a1i	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∩ ( ∪ 𝑆 ∖ 𝐹 ) ) = ( ( 𝐸 ∩ ∪ 𝑆 ) ∖ 𝐹 ) )
3		elssuni	⊢ ( 𝐸 ∈ 𝑆 → 𝐸 ⊆ ∪ 𝑆 )
4		df-ss	⊢ ( 𝐸 ⊆ ∪ 𝑆 ↔ ( 𝐸 ∩ ∪ 𝑆 ) = 𝐸 )
5	3 4	sylib	⊢ ( 𝐸 ∈ 𝑆 → ( 𝐸 ∩ ∪ 𝑆 ) = 𝐸 )
6	5	difeq1d	⊢ ( 𝐸 ∈ 𝑆 → ( ( 𝐸 ∩ ∪ 𝑆 ) ∖ 𝐹 ) = ( 𝐸 ∖ 𝐹 ) )
7	6	3ad2ant2	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ( 𝐸 ∩ ∪ 𝑆 ) ∖ 𝐹 ) = ( 𝐸 ∖ 𝐹 ) )
8	2 7	eqtr2d	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∖ 𝐹 ) = ( 𝐸 ∩ ( ∪ 𝑆 ∖ 𝐹 ) ) )
9		simp1	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → 𝑆 ∈ SAlg )
10		simp2	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → 𝐸 ∈ 𝑆 )
11		saldifcl	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐹 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐹 ) ∈ 𝑆 )
12	11	3adant2	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐹 ) ∈ 𝑆 )
13		salincl	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ ( ∪ 𝑆 ∖ 𝐹 ) ∈ 𝑆 ) → ( 𝐸 ∩ ( ∪ 𝑆 ∖ 𝐹 ) ) ∈ 𝑆 )
14	9 10 12 13	syl3anc	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∩ ( ∪ 𝑆 ∖ 𝐹 ) ) ∈ 𝑆 )
15	8 14	eqeltrd	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐸 ∖ 𝐹 ) ∈ 𝑆 )