Metamath Proof Explorer


Theorem pwcntmeas

Description: The counting measure is a measure on any power set. (Contributed by Thierry Arnoux, 24-Jan-2017)

Ref Expression
Assertion pwcntmeas O V . 𝒫 O measures 𝒫 O

Proof

Step Hyp Ref Expression
1 pwsiga O V 𝒫 O sigAlgebra O
2 elrnsiga 𝒫 O sigAlgebra O 𝒫 O ran sigAlgebra
3 cntmeas 𝒫 O ran sigAlgebra . 𝒫 O measures 𝒫 O
4 1 2 3 3syl O V . 𝒫 O measures 𝒫 O