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 e. V -> ( # |` ~P O ) e. ( measures ` ~P O ) )

Proof

Step Hyp Ref Expression
1 pwsiga 
 |-  ( O e. V -> ~P O e. ( sigAlgebra ` O ) )
2 elrnsiga 
 |-  ( ~P O e. ( sigAlgebra ` O ) -> ~P O e. U. ran sigAlgebra )
3 cntmeas 
 |-  ( ~P O e. U. ran sigAlgebra -> ( # |` ~P O ) e. ( measures ` ~P O ) )
4 1 2 3 3syl 
 |-  ( O e. V -> ( # |` ~P O ) e. ( measures ` ~P O ) )