Theorem pwcntmeas

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

	Ref	Expression
Assertion	pwcntmeas	⊢ ( 𝑂 ∈ 𝑉 → ( ♯ ↾ 𝒫 𝑂 ) ∈ ( measures ‘ 𝒫 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		pwsiga	⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ ( sigAlgebra ‘ 𝑂 ) )
2		elrnsiga	⊢ ( 𝒫 𝑂 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝒫 𝑂 ∈ ∪ ran sigAlgebra )
3		cntmeas	⊢ ( 𝒫 𝑂 ∈ ∪ ran sigAlgebra → ( ♯ ↾ 𝒫 𝑂 ) ∈ ( measures ‘ 𝒫 𝑂 ) )
4	1 2 3	3syl	⊢ ( 𝑂 ∈ 𝑉 → ( ♯ ↾ 𝒫 𝑂 ) ∈ ( measures ‘ 𝒫 𝑂 ) )