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	|- ( ph -> X e. V )
	salgenss.g	|- G = ( SalGen ` X )
	salgenss.s	|- ( ph -> S e. SAlg )
	salgenss.i	|- ( ph -> X C_ S )
	salgenss.u	|- ( ph -> U. S = U. X )
Assertion	salgenss	|- ( ph -> G C_ S )

Proof

Step	Hyp	Ref	Expression
1		salgenss.x	|- ( ph -> X e. V )
2		salgenss.g	|- G = ( SalGen ` X )
3		salgenss.s	|- ( ph -> S e. SAlg )
4		salgenss.i	|- ( ph -> X C_ S )
5		salgenss.u	|- ( ph -> U. S = U. X )
6	2	a1i	|- ( ph -> G = ( SalGen ` X ) )
7		salgenval	|- ( X e. V -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
8	1 7	syl	|- ( ph -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
9	6 8	eqtrd	|- ( ph -> G = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
10	5 4	jca	|- ( ph -> ( U. S = U. X /\ X C_ S ) )
11	3 10	jca	|- ( ph -> ( S e. SAlg /\ ( U. S = U. X /\ X C_ S ) ) )
12		unieq	|- ( s = S -> U. s = U. S )
13	12	eqeq1d	|- ( s = S -> ( U. s = U. X <-> U. S = U. X ) )
14		sseq2	|- ( s = S -> ( X C_ s <-> X C_ S ) )
15	13 14	anbi12d	|- ( s = S -> ( ( U. s = U. X /\ X C_ s ) <-> ( U. S = U. X /\ X C_ S ) ) )
16	15	elrab	|- ( S e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> ( S e. SAlg /\ ( U. S = U. X /\ X C_ S ) ) )
17	11 16	sylibr	|- ( ph -> S e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
18		intss1	|- ( S e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } C_ S )
19	17 18	syl	|- ( ph -> |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } C_ S )
20	9 19	eqsstrd	|- ( ph -> G C_ S )