Theorem salgenss

Description: The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set. Proposition 111G (b) of Fremlin1 p. 13. Notice that the condition "on the same base set" is needed, see the counterexample salgensscntex , where a sigma-algebra is shown that includes a set, but does not include the sigma-algebra generated (the key is that its base set is larger than the base set of the generating set). (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salgenss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	salgenss.g	⊢ 𝐺 = ( SalGen ‘ 𝑋 )
	salgenss.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	salgenss.i	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
	salgenss.u	⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝑋 )
Assertion	salgenss	⊢ ( 𝜑 → 𝐺 ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		salgenss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		salgenss.g	⊢ 𝐺 = ( SalGen ‘ 𝑋 )
3		salgenss.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		salgenss.i	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
5		salgenss.u	⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝑋 )
6	2	a1i	⊢ ( 𝜑 → 𝐺 = ( SalGen ‘ 𝑋 ) )
7		salgenval	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
8	1 7	syl	⊢ ( 𝜑 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
9	6 8	eqtrd	⊢ ( 𝜑 → 𝐺 = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
10	5 4	jca	⊢ ( 𝜑 → ( ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) )
11	3 10	jca	⊢ ( 𝜑 → ( 𝑆 ∈ SAlg ∧ ( ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ) )
12		unieq	⊢ ( 𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆 )
13	12	eqeq1d	⊢ ( 𝑠 = 𝑆 → ( ∪ 𝑠 = ∪ 𝑋 ↔ ∪ 𝑆 = ∪ 𝑋 ) )
14		sseq2	⊢ ( 𝑠 = 𝑆 → ( 𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑆 ) )
15	13 14	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) ↔ ( ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ) )
16	15	elrab	⊢ ( 𝑆 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ( 𝑆 ∈ SAlg ∧ ( ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) ) )
17	11 16	sylibr	⊢ ( 𝜑 → 𝑆 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
18		intss1	⊢ ( 𝑆 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ⊆ 𝑆 )
19	17 18	syl	⊢ ( 𝜑 → ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ⊆ 𝑆 )
20	9 19	eqsstrd	⊢ ( 𝜑 → 𝐺 ⊆ 𝑆 )