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 43553
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 43552 . 2 class SAlg
2 c0 4251 . . . . 5 class
3 vx . . . . . 6 setvar 𝑥
43cv 1542 . . . . 5 class 𝑥
52, 4wcel 2111 . . . 4 wff ∅ ∈ 𝑥
64cuni 4833 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1542 . . . . . . 7 class 𝑦
96, 8cdif 3877 . . . . . 6 class ( 𝑥𝑦)
109, 4wcel 2111 . . . . 5 wff ( 𝑥𝑦) ∈ 𝑥
1110, 7, 4wral 3062 . . . 4 wff 𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥
12 com 7662 . . . . . . 7 class ω
13 cdom 8644 . . . . . . 7 class
148, 12, 13wbr 5067 . . . . . 6 wff 𝑦 ≼ ω
158cuni 4833 . . . . . . 7 class 𝑦
1615, 4wcel 2111 . . . . . 6 wff 𝑦𝑥
1714, 16wi 4 . . . . 5 wff (𝑦 ≼ ω → 𝑦𝑥)
184cpw 4527 . . . . 5 class 𝒫 𝑥
1917, 7, 18wral 3062 . . . 4 wff 𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥)
205, 11, 19w3a 1089 . . 3 wff (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))
2120, 3cab 2715 . 2 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))}
221, 21wceq 1543 1 wff SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 ( 𝑥𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → 𝑦𝑥))}
Colors of variables: wff setvar class
This definition is referenced by:  issal  43558
  Copyright terms: Public domain W3C validator