Definition df-sigagen

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csigagen	⊢ sigaGen
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		csiga	⊢ sigAlgebra
5	1	cv	⊢ 𝑥
6	5	cuni	⊢ ∪ 𝑥
7	6 4	cfv	⊢ ( sigAlgebra ‘ ∪ 𝑥 )
8	3	cv	⊢ 𝑠
9	5 8	wss	⊢ 𝑥 ⊆ 𝑠
10	9 3 7	crab	⊢ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 }
11	10	cint	⊢ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 }
12	1 2 11	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 } )
13	0 12	wceq	⊢ sigaGen = ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 } )