Metamath Proof Explorer

Definition df-salg

Description: Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion df-salg ⊢ SAlg = x | ∅ ∈ x ∧ ∀ y ∈ x ⋃ x ∖ y ∈ x ∧ ∀ y ∈ 𝒫 x y ≼ ω → ⋃ y ∈ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 csalg class SAlg
1 vx setvar x
2 c0 class ∅
3 1 cv setvar x
4 2 3 wcel wff ∅ ∈ x
5 vy setvar y
6 3 cuni class ⋃ x
7 5 cv setvar y
8 6 7 cdif class ⋃ x ∖ y
9 8 3 wcel wff ⋃ x ∖ y ∈ x
10 9 5 3 wral wff ∀ y ∈ x ⋃ x ∖ y ∈ x
11 3 cpw class 𝒫 x
12 cdom class ≼
13 com class ω
14 7 13 12 wbr wff y ≼ ω
15 7 cuni class ⋃ y
16 15 3 wcel wff ⋃ y ∈ x
17 14 16 wi wff y ≼ ω → ⋃ y ∈ x
18 17 5 11 wral wff ∀ y ∈ 𝒫 x y ≼ ω → ⋃ y ∈ x
19 4 10 18 w3a wff ∅ ∈ x ∧ ∀ y ∈ x ⋃ x ∖ y ∈ x ∧ ∀ y ∈ 𝒫 x y ≼ ω → ⋃ y ∈ x
20 19 1 cab class x | ∅ ∈ x ∧ ∀ y ∈ x ⋃ x ∖ y ∈ x ∧ ∀ y ∈ 𝒫 x y ≼ ω → ⋃ y ∈ x
21 0 20 wceq wff SAlg = x | ∅ ∈ x ∧ ∀ y ∈ x ⋃ x ∖ y ∈ x ∧ ∀ y ∈ 𝒫 x y ≼ ω → ⋃ y ∈ x