mea0

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

		Ref	Expression
	Hypothesis	mea0.1	$⊢ φ \to M \in Meas$
	Assertion	mea0	$⊢ φ \to M (\emptyset) = 0$

Step	Hyp	Ref	Expression
1		mea0.1	$⊢ φ \to M \in Meas$
2		ismea	$⊢ M \in Meas \leftrightarrow (((M : dom M ⟶ [0, +∞] \land dom M \in SAlg) \land M (\emptyset) = 0) \land \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = sum^({M ↾}_{x})))$
3	1 2	sylib	$⊢ φ \to (((M : dom M ⟶ [0, +∞] \land dom M \in SAlg) \land M (\emptyset) = 0) \land \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = sum^({M ↾}_{x})))$
4	3	simplrd	$⊢ φ \to M (\emptyset) = 0$

Metamath Proof Explorer