Theorem saldifcl

Description: The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	saldifcl	|- ( ( S e. SAlg /\ E e. S ) -> ( U. S \ E ) e. S )

Proof

Step	Hyp	Ref	Expression
1		difeq2	|- ( y = E -> ( U. S \ y ) = ( U. S \ E ) )
2	1	eleq1d	|- ( y = E -> ( ( U. S \ y ) e. S <-> ( U. S \ E ) e. S ) )
3		issal	|- ( S e. SAlg -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
4	3	ibi	|- ( S e. SAlg -> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) )
5	4	simp2d	|- ( S e. SAlg -> A. y e. S ( U. S \ y ) e. S )
6	5	adantr	|- ( ( S e. SAlg /\ E e. S ) -> A. y e. S ( U. S \ y ) e. S )
7		simpr	|- ( ( S e. SAlg /\ E e. S ) -> E e. S )
8	2 6 7	rspcdva	|- ( ( S e. SAlg /\ E e. S ) -> ( U. S \ E ) e. S )