Metamath Proof Explorer


Theorem difelsiga

Description: A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016)

Ref Expression
Assertion difelsiga ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → ( 𝐴𝐵 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 simp2 ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → 𝐴𝑆 )
2 elssuni ( 𝐴𝑆𝐴 𝑆 )
3 difin2 ( 𝐴 𝑆 → ( 𝐴𝐵 ) = ( ( 𝑆𝐵 ) ∩ 𝐴 ) )
4 1 2 3 3syl ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → ( 𝐴𝐵 ) = ( ( 𝑆𝐵 ) ∩ 𝐴 ) )
5 isrnsigau ( 𝑆 ran sigAlgebra → ( 𝑆 ⊆ 𝒫 𝑆 ∧ ( 𝑆𝑆 ∧ ∀ 𝑥𝑆 ( 𝑆𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → 𝑥𝑆 ) ) ) )
6 5 simprd ( 𝑆 ran sigAlgebra → ( 𝑆𝑆 ∧ ∀ 𝑥𝑆 ( 𝑆𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → 𝑥𝑆 ) ) )
7 6 simp2d ( 𝑆 ran sigAlgebra → ∀ 𝑥𝑆 ( 𝑆𝑥 ) ∈ 𝑆 )
8 difeq2 ( 𝑥 = 𝐵 → ( 𝑆𝑥 ) = ( 𝑆𝐵 ) )
9 8 eleq1d ( 𝑥 = 𝐵 → ( ( 𝑆𝑥 ) ∈ 𝑆 ↔ ( 𝑆𝐵 ) ∈ 𝑆 ) )
10 9 rspccva ( ( ∀ 𝑥𝑆 ( 𝑆𝑥 ) ∈ 𝑆𝐵𝑆 ) → ( 𝑆𝐵 ) ∈ 𝑆 )
11 7 10 sylan ( ( 𝑆 ran sigAlgebra ∧ 𝐵𝑆 ) → ( 𝑆𝐵 ) ∈ 𝑆 )
12 11 3adant2 ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → ( 𝑆𝐵 ) ∈ 𝑆 )
13 intprg ( ( ( 𝑆𝐵 ) ∈ 𝑆𝐴𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } = ( ( 𝑆𝐵 ) ∩ 𝐴 ) )
14 12 1 13 syl2anc ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } = ( ( 𝑆𝐵 ) ∩ 𝐴 ) )
15 4 14 eqtr4d ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → ( 𝐴𝐵 ) = { ( 𝑆𝐵 ) , 𝐴 } )
16 simp1 ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → 𝑆 ran sigAlgebra )
17 prssi ( ( ( 𝑆𝐵 ) ∈ 𝑆𝐴𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } ⊆ 𝑆 )
18 12 1 17 syl2anc ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } ⊆ 𝑆 )
19 prex { ( 𝑆𝐵 ) , 𝐴 } ∈ V
20 19 elpw ( { ( 𝑆𝐵 ) , 𝐴 } ∈ 𝒫 𝑆 ↔ { ( 𝑆𝐵 ) , 𝐴 } ⊆ 𝑆 )
21 18 20 sylibr ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } ∈ 𝒫 𝑆 )
22 prct ( ( ( 𝑆𝐵 ) ∈ 𝑆𝐴𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } ≼ ω )
23 12 1 22 syl2anc ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } ≼ ω )
24 prnzg ( ( 𝑆𝐵 ) ∈ 𝑆 → { ( 𝑆𝐵 ) , 𝐴 } ≠ ∅ )
25 12 24 syl ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } ≠ ∅ )
26 sigaclci ( ( ( 𝑆 ran sigAlgebra ∧ { ( 𝑆𝐵 ) , 𝐴 } ∈ 𝒫 𝑆 ) ∧ ( { ( 𝑆𝐵 ) , 𝐴 } ≼ ω ∧ { ( 𝑆𝐵 ) , 𝐴 } ≠ ∅ ) ) → { ( 𝑆𝐵 ) , 𝐴 } ∈ 𝑆 )
27 16 21 23 25 26 syl22anc ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → { ( 𝑆𝐵 ) , 𝐴 } ∈ 𝑆 )
28 15 27 eqeltrd ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆𝐵𝑆 ) → ( 𝐴𝐵 ) ∈ 𝑆 )