Metamath Proof Explorer


Theorem sgon

Description: A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017)

Ref Expression
Assertion sgon ( 𝑆 ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 eqid 𝑆 = 𝑆
2 issgon ( 𝑆 ∈ ( sigAlgebra ‘ 𝑆 ) ↔ ( 𝑆 ran sigAlgebra ∧ 𝑆 = 𝑆 ) )
3 2 biimpri ( ( 𝑆 ran sigAlgebra ∧ 𝑆 = 𝑆 ) → 𝑆 ∈ ( sigAlgebra ‘ 𝑆 ) )
4 1 3 mpan2 ( 𝑆 ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ 𝑆 ) )