Metamath Proof Explorer

Theorem mea0

Description: The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis mea0.1 
|- ( ph -> M e. Meas )
Assertion mea0 
|- ( ph -> ( M ` (/) ) = 0 )

Proof

Step Hyp Ref Expression
1 mea0.1 
 |-  ( ph -> M e. Meas )
2 ismea 
 |-  ( M e. Meas <-> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
3 1 2 sylib 
 |-  ( ph -> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
4 3 simplrd 
 |-  ( ph -> ( M ` (/) ) = 0 )