Metamath Proof Explorer

Definition df-siga

Description: Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using S and O as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016)

Ref Expression
Assertion df-siga ⊢ sigAlgebra = o ∈ V ⟼ s | s ⊆ 𝒫 o ∧ o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s

Detailed syntax breakdown

Step Hyp Ref Expression
0 csiga class sigAlgebra
1 vo setvar o
2 cvv class V
3 vs setvar s
4 3 cv setvar s
5 1 cv setvar o
6 5 cpw class 𝒫 o
7 4 6 wss wff s ⊆ 𝒫 o
8 5 4 wcel wff o ∈ s
9 vx setvar x
10 9 cv setvar x
11 5 10 cdif class o ∖ x
12 11 4 wcel wff o ∖ x ∈ s
13 12 9 4 wral wff ∀ x ∈ s o ∖ x ∈ s
14 4 cpw class 𝒫 s
15 cdom class ≼
16 com class ω
17 10 16 15 wbr wff x ≼ ω
18 10 cuni class ⋃ x
19 18 4 wcel wff ⋃ x ∈ s
20 17 19 wi wff x ≼ ω → ⋃ x ∈ s
21 20 9 14 wral wff ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s
22 8 13 21 w3a wff o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s
23 7 22 wa wff s ⊆ 𝒫 o ∧ o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s
24 23 3 cab class s | s ⊆ 𝒫 o ∧ o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s
25 1 2 24 cmpt class o ∈ V ⟼ s | s ⊆ 𝒫 o ∧ o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s
26 0 25 wceq wff sigAlgebra = o ∈ V ⟼ s | s ⊆ 𝒫 o ∧ o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s