Metamath Proof Explorer


Theorem isrnsigau

Description: The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016)

Ref Expression
Assertion isrnsigau S ran sigAlgebra S 𝒫 S S S x S S x S x 𝒫 S x ω x S

Proof

Step Hyp Ref Expression
1 sgon S ran sigAlgebra S sigAlgebra S
2 elex S ran sigAlgebra S V
3 issiga S V S sigAlgebra S S 𝒫 S S S x S S x S x 𝒫 S x ω x S
4 2 3 syl S ran sigAlgebra S sigAlgebra S S 𝒫 S S S x S S x S x 𝒫 S x ω x S
5 1 4 mpbid S ran sigAlgebra S 𝒫 S S S x S S x S x 𝒫 S x ω x S