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