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 ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 difun1 ⊢ ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐴 ) ∪ 𝐵 ) ) = ( ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐴 ) ) ∖ 𝐵 )
2 1 a1i ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐴 ) ∪ 𝐵 ) ) = ( ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐴 ) ) ∖ 𝐵 ) )
3 simp1 ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
4 simp2 ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
5 elsigass ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ⊆ ∪ 𝑆 )
6 3 4 5 syl2anc ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐴 ⊆ ∪ 𝑆 )
7 dfss4 ⊢ ( 𝐴 ⊆ ∪ 𝑆 ↔ ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐴 ) ) = 𝐴 )
8 6 7 sylib ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐴 ) ) = 𝐴 )
9 8 difeq1d ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐴 ) ) ∖ 𝐵 ) = ( 𝐴 ∖ 𝐵 ) )
10 2 9 eqtrd ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐴 ) ∪ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 ) )
11 difunielsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐴 ) ∈ 𝑆 )
12 3 4 11 syl2anc ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐴 ) ∈ 𝑆 )
13 simp3 ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐵 ∈ 𝑆 )
14 unelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ( ∪ 𝑆 ∖ 𝐴 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ∪ 𝑆 ∖ 𝐴 ) ∪ 𝐵 ) ∈ 𝑆 )
15 3 12 13 14 syl3anc ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ∪ 𝑆 ∖ 𝐴 ) ∪ 𝐵 ) ∈ 𝑆 )
16 difunielsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ( ( ∪ 𝑆 ∖ 𝐴 ) ∪ 𝐵 ) ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐴 ) ∪ 𝐵 ) ) ∈ 𝑆 )
17 3 15 16 syl2anc ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ( ∪ 𝑆 ∖ 𝐴 ) ∪ 𝐵 ) ) ∈ 𝑆 )
18 10 17 eqeltrrd ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 )