Definition df-sigagen 34175

Description: Define the sigma-algebra generated by a given collection of sets as the intersection of all sigma-algebra containing that set. (Contributed by Thierry Arnoux, 27-Dec-2016.)

Assertion

Ref	Expression
df-sigagen	⊢ sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠})

Distinct variable group:   𝑥,𝑠

Detailed syntax breakdown of Definition df-sigagen

Step	Hyp	Ref	Expression
1		csigagen 34174	. 2 class sigaGen
2		vx	. . 3 setvar 𝑥
3		cvv 3464	. . 3 class V
4	2	cv 1539	. . . . . 6 class 𝑥
5		vs	. . . . . . 7 setvar 𝑠
6	5	cv 1539	. . . . . 6 class 𝑠
7	4, 6	wss 3931	. . . . 5 wff 𝑥 ⊆ 𝑠
8	4	cuni 4888	. . . . . 6 class ∪ 𝑥
9		csiga 34144	. . . . . 6 class sigAlgebra
10	8, 9	cfv 6536	. . . . 5 class (sigAlgebra‘∪ 𝑥)
11	7, 5, 10	crab 3420	. . . 4 class {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠}
12	11	cint 4927	. . 3 class ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠}
13	2, 3, 12	cmpt 5206	. 2 class (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠})
14	1, 13	wceq 1540	1 wff sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠})

This definition is referenced by:  sigagenval  34176  dmsigagen  34180  brsiga  34219