Theorem issal

Description: Express the predicate " S is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	issal	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝑥 = 𝑆 → ( ∅ ∈ 𝑥 ↔ ∅ ∈ 𝑆 ) )
2		id	⊢ ( 𝑥 = 𝑆 → 𝑥 = 𝑆 )
3		unieq	⊢ ( 𝑥 = 𝑆 → ∪ 𝑥 = ∪ 𝑆 )
4	3	difeq1d	⊢ ( 𝑥 = 𝑆 → ( ∪ 𝑥 ∖ 𝑦 ) = ( ∪ 𝑆 ∖ 𝑦 ) )
5	4 2	eleq12d	⊢ ( 𝑥 = 𝑆 → ( ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥 ↔ ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ) )
6	2 5	raleqbidv	⊢ ( 𝑥 = 𝑆 → ( ∀ 𝑦 ∈ 𝑥 ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ) )
7		pweq	⊢ ( 𝑥 = 𝑆 → 𝒫 𝑥 = 𝒫 𝑆 )
8		eleq2	⊢ ( 𝑥 = 𝑆 → ( ∪ 𝑦 ∈ 𝑥 ↔ ∪ 𝑦 ∈ 𝑆 ) )
9	8	imbi2d	⊢ ( 𝑥 = 𝑆 → ( ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) )
10	7 9	raleqbidv	⊢ ( 𝑥 = 𝑆 → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) )
11	1 6 10	3anbi123d	⊢ ( 𝑥 = 𝑆 → ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 ) ) ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
12		df-salg	⊢ SAlg = { 𝑥 ∣ ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 ) ) }
13	11 12	elab2g	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )