Definition df-salgen

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 . 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 . (Contributed by Glauco Siliprandi, 17-Aug-2020) (Revised by Glauco Siliprandi, 1-Jan-2021)

	Ref	Expression
Assertion	df-salgen	⊢ SalGen = ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csalgen	⊢ SalGen
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		csalg	⊢ SAlg
5	3	cv	⊢ 𝑠
6	5	cuni	⊢ ∪ 𝑠
7	1	cv	⊢ 𝑥
8	7	cuni	⊢ ∪ 𝑥
9	6 8	wceq	⊢ ∪ 𝑠 = ∪ 𝑥
10	7 5	wss	⊢ 𝑥 ⊆ 𝑠
11	9 10	wa	⊢ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 )
12	11 3 4	crab	⊢ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) }
13	12	cint	⊢ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) }
14	1 2 13	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) } )
15	0 14	wceq	⊢ SalGen = ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) } )