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 42479
 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 42478 . 2 class SAlg
2 c0 4295 . . . . 5 class
3 vx . . . . . 6 setvar 𝑥
43cv 1529 . . . . 5 class 𝑥
52, 4wcel 2107 . . . 4 wff ∅ ∈ 𝑥
64cuni 4837 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1529 . . . . . . 7 class 𝑦
96, 8cdif 3937 . . . . . 6 class ( 𝑥𝑦)
109, 4wcel 2107 . . . . 5 wff ( 𝑥𝑦) ∈ 𝑥
1110, 7, 4wral 3143 . . . 4 wff 𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥
12 com 7573 . . . . . . 7 class ω
13 cdom 8501 . . . . . . 7 class
148, 12, 13wbr 5063 . . . . . 6 wff 𝑦 ≼ ω
158cuni 4837 . . . . . . 7 class 𝑦
1615, 4wcel 2107 . . . . . 6 wff 𝑦𝑥
1714, 16wi 4 . . . . 5 wff (𝑦 ≼ ω → 𝑦𝑥)
184cpw 4542 . . . . 5 class 𝒫 𝑥
1917, 7, 18wral 3143 . . . 4 wff 𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥)
205, 11, 19w3a 1081 . . 3 wff (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))
2120, 3cab 2804 . 2 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))}
221, 21wceq 1530 1 wff SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))}
 Colors of variables: wff setvar class This definition is referenced by:  issal  42484
 Copyright terms: Public domain W3C validator