Metamath Proof Explorer


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=SalGenX
Assertion sssalgen XVXS

Proof

Step Hyp Ref Expression
1 sssalgen.1 S=SalGenX
2 ssint XsSAlg|s=XXstsSAlg|s=XXsXt
3 unieq s=ts=t
4 3 eqeq1d s=ts=Xt=X
5 sseq2 s=tXsXt
6 4 5 anbi12d s=ts=XXst=XXt
7 6 elrab tsSAlg|s=XXstSAlgt=XXt
8 7 biimpi tsSAlg|s=XXstSAlgt=XXt
9 8 simprrd tsSAlg|s=XXsXt
10 2 9 mprgbir XsSAlg|s=XXs
11 10 a1i XVXsSAlg|s=XXs
12 salgenval XVSalGenX=sSAlg|s=XXs
13 1 12 eqtr2id XVsSAlg|s=XXs=S
14 11 13 sseqtrd XVXS