Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-salg Structured version   Visualization version   GIF version

Definition df-salg 39857
Description: Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Assertion
Ref Expression
df-salg SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))}
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-salg
StepHypRef Expression
1 csalg 39856 . 2 class SAlg
2 c0 3896 . . . . 5 class
3 vx . . . . . 6 setvar 𝑥
43cv 1479 . . . . 5 class 𝑥
52, 4wcel 1987 . . . 4 wff ∅ ∈ 𝑥
64cuni 4407 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1479 . . . . . . 7 class 𝑦
96, 8cdif 3556 . . . . . 6 class ( 𝑥𝑦)
109, 4wcel 1987 . . . . 5 wff ( 𝑥𝑦) ∈ 𝑥
1110, 7, 4wral 2907 . . . 4 wff 𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥
12 com 7019 . . . . . . 7 class ω
13 cdom 7904 . . . . . . 7 class
148, 12, 13wbr 4618 . . . . . 6 wff 𝑦 ≼ ω
158cuni 4407 . . . . . . 7 class 𝑦
1615, 4wcel 1987 . . . . . 6 wff 𝑦𝑥
1714, 16wi 4 . . . . 5 wff (𝑦 ≼ ω → 𝑦𝑥)
184cpw 4135 . . . . 5 class 𝒫 𝑥
1917, 7, 18wral 2907 . . . 4 wff 𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥)
205, 11, 19w3a 1036 . . 3 wff (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))
2120, 3cab 2607 . 2 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))}
221, 21wceq 1480 1 wff SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))}
Colors of variables: wff setvar class
This definition is referenced by:  issal  39862
  Copyright terms: Public domain W3C validator