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

Proof

Step	Hyp	Ref	Expression
1		difeq2	⊢ ( 𝑦 = 𝐸 → ( ∪ 𝑆 ∖ 𝑦 ) = ( ∪ 𝑆 ∖ 𝐸 ) )
2	1	eleq1d	⊢ ( 𝑦 = 𝐸 → ( ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 ) )
3		issal	⊢ ( 𝑆 ∈ SAlg → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
4	3	ibi	⊢ ( 𝑆 ∈ SAlg → ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) )
5	4	simp2d	⊢ ( 𝑆 ∈ SAlg → ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 )
6	5	adantr	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 )
7		simpr	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → 𝐸 ∈ 𝑆 )
8	2 6 7	rspcdva	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )