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 ( 𝐴𝑉 ( sigaGen ‘ 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 sigagensiga ( 𝐴𝑉 → ( sigaGen ‘ 𝐴 ) ∈ ( sigAlgebra ‘ 𝐴 ) )
2 issgon ( ( sigaGen ‘ 𝐴 ) ∈ ( sigAlgebra ‘ 𝐴 ) ↔ ( ( sigaGen ‘ 𝐴 ) ∈ ran sigAlgebra ∧ 𝐴 = ( sigaGen ‘ 𝐴 ) ) )
3 1 2 sylib ( 𝐴𝑉 → ( ( sigaGen ‘ 𝐴 ) ∈ ran sigAlgebra ∧ 𝐴 = ( sigaGen ‘ 𝐴 ) ) )
4 3 simprd ( 𝐴𝑉 𝐴 = ( sigaGen ‘ 𝐴 ) )
5 4 eqcomd ( 𝐴𝑉 ( sigaGen ‘ 𝐴 ) = 𝐴 )