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

Definition df-salgen 39837
Description: Define the sigma-algebra generated by a given set. Definition 111G (b) of [Fremlin1] p. 13. The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set, see dfsalgen2 39863. The base set of the sigma-algebras used for the intersection needs to be the same, otherwise the resulting set is not guaranteed to be a sigma-algebra, as shown in the counterexample salgencntex 39865. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.)
Assertion
Ref Expression
df-salgen SalGen = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ( 𝑠 = 𝑥𝑥𝑠)})
Distinct variable group:   𝑥,𝑠

Detailed syntax breakdown of Definition df-salgen
StepHypRef Expression
1 csalgen 39836 . 2 class SalGen
2 vx . . 3 setvar 𝑥
3 cvv 3186 . . 3 class V
4 vs . . . . . . . . 9 setvar 𝑠
54cv 1479 . . . . . . . 8 class 𝑠
65cuni 4402 . . . . . . 7 class 𝑠
72cv 1479 . . . . . . . 8 class 𝑥
87cuni 4402 . . . . . . 7 class 𝑥
96, 8wceq 1480 . . . . . 6 wff 𝑠 = 𝑥
107, 5wss 3555 . . . . . 6 wff 𝑥𝑠
119, 10wa 384 . . . . 5 wff ( 𝑠 = 𝑥𝑥𝑠)
12 csalg 39832 . . . . 5 class SAlg
1311, 4, 12crab 2911 . . . 4 class {𝑠 ∈ SAlg ∣ ( 𝑠 = 𝑥𝑥𝑠)}
1413cint 4440 . . 3 class {𝑠 ∈ SAlg ∣ ( 𝑠 = 𝑥𝑥𝑠)}
152, 3, 14cmpt 4673 . 2 class (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ( 𝑠 = 𝑥𝑥𝑠)})
161, 15wceq 1480 1 wff SalGen = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ( 𝑠 = 𝑥𝑥𝑠)})
Colors of variables: wff setvar class
This definition is referenced by:  salgenval  39845
  Copyright terms: Public domain W3C validator