Metamath Proof Explorer

Theorem difelsiga

Description: A sigma-algebra is closed under class differences. The proof goes through difunielsiga and unelsiga rather than countable intersection, and so does not use ax-ac . (Contributed by Thierry Arnoux, 13-Sep-2016) (Proof shortened by Vincent Gonzalez, 17-Aug-2026)

Ref Expression
Assertion difelsiga 
|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )

Proof

Step Hyp Ref Expression
1 difun1 
 |-  ( U. S \ ( ( U. S \ A ) u. B ) ) = ( ( U. S \ ( U. S \ A ) ) \ B )
2 1 a1i 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( U. S \ ( ( U. S \ A ) u. B ) ) = ( ( U. S \ ( U. S \ A ) ) \ B ) )
3 simp1 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> S e. U. ran sigAlgebra )
4 simp2 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> A e. S )
5 elsigass 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A C_ U. S )
6 3 4 5 syl2anc 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> A C_ U. S )
7 dfss4 
 |-  ( A C_ U. S <-> ( U. S \ ( U. S \ A ) ) = A )
8 6 7 sylib 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( U. S \ ( U. S \ A ) ) = A )
9 8 difeq1d 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( ( U. S \ ( U. S \ A ) ) \ B ) = ( A \ B ) )
10 2 9 eqtrd 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( U. S \ ( ( U. S \ A ) u. B ) ) = ( A \ B ) )
11 difunielsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( U. S \ A ) e. S )
12 3 4 11 syl2anc 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( U. S \ A ) e. S )
13 simp3 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> B e. S )
14 unelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ ( U. S \ A ) e. S /\ B e. S ) -> ( ( U. S \ A ) u. B ) e. S )
15 3 12 13 14 syl3anc 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( ( U. S \ A ) u. B ) e. S )
16 difunielsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ ( ( U. S \ A ) u. B ) e. S ) -> ( U. S \ ( ( U. S \ A ) u. B ) ) e. S )
17 3 15 16 syl2anc 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( U. S \ ( ( U. S \ A ) u. B ) ) e. S )
18 10 17 eqeltrrd 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )