Theorem measfrge0

Description: A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016)

	Ref	Expression
Assertion	measfrge0	⊢ ( 𝑀 ∈ ( 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	simp1d	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )