Definition df-salgen 41471

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 41497. 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 41499. (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

Step	Hyp	Ref	Expression
1		csalgen 41470	. 2 class SalGen
2		vx	. . 3 setvar 𝑥
3		cvv 3398	. . 3 class V
4		vs	. . . . . . . . 9 setvar 𝑠
5	4	cv 1600	. . . . . . . 8 class 𝑠
6	5	cuni 4673	. . . . . . 7 class ∪ 𝑠
7	2	cv 1600	. . . . . . . 8 class 𝑥
8	7	cuni 4673	. . . . . . 7 class ∪ 𝑥
9	6, 8	wceq 1601	. . . . . 6 wff ∪ 𝑠 = ∪ 𝑥
10	7, 5	wss 3792	. . . . . 6 wff 𝑥 ⊆ 𝑠
11	9, 10	wa 386	. . . . 5 wff (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)
12		csalg 41466	. . . . 5 class SAlg
13	11, 4, 12	crab 3094	. . . 4 class {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)}
14	13	cint 4712	. . 3 class ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)}
15	2, 3, 14	cmpt 4967	. 2 class (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)})
16	1, 15	wceq 1601	1 wff SalGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)})

This definition is referenced by:  salgenval  41479