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