Metamath Proof Explorer


Theorem unisg

Description: The sigma-algebra generated by a collection A is a sigma-algebra on U. A . (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion unisg AV𝛔A=A

Proof

Step Hyp Ref Expression
1 sigagensiga AV𝛔AsigAlgebraA
2 issgon 𝛔AsigAlgebraA𝛔AransigAlgebraA=𝛔A
3 1 2 sylib AV𝛔AransigAlgebraA=𝛔A
4 3 simprd AVA=𝛔A
5 4 eqcomd AV𝛔A=A