Theorem sssalgen

Description: A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypothesis	sssalgen.1	|- S = ( SalGen ` X )
Assertion	sssalgen	|- ( X e. V -> X C_ S )

Proof

Step	Hyp	Ref	Expression
1		sssalgen.1	|- S = ( SalGen ` X )
2		ssint	|- ( X C_ |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> A. t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } X C_ t )
3		unieq	|- ( s = t -> U. s = U. t )
4	3	eqeq1d	|- ( s = t -> ( U. s = U. X <-> U. t = U. X ) )
5		sseq2	|- ( s = t -> ( X C_ s <-> X C_ t ) )
6	4 5	anbi12d	|- ( s = t -> ( ( U. s = U. X /\ X C_ s ) <-> ( U. t = U. X /\ X C_ t ) ) )
7	6	elrab	|- ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> ( t e. SAlg /\ ( U. t = U. X /\ X C_ t ) ) )
8	7	biimpi	|- ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> ( t e. SAlg /\ ( U. t = U. X /\ X C_ t ) ) )
9	8	simprrd	|- ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> X C_ t )
10	2 9	mprgbir	|- X C_ |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) }
11	10	a1i	|- ( X e. V -> X C_ |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
12		salgenval	|- ( X e. V -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
13	1 12	syl5req	|- ( X e. V -> |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } = S )
14	11 13	sseqtrd	|- ( X e. V -> X C_ S )