Theorem measvnul

Description: The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016)

	Ref	Expression
Assertion	measvnul	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		measbase	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
2		ismeas	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) ) )
3	1 2	syl	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) ) )
4	3	ibi	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) )
5	4	simp2d	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 )