Theorem meaf

Description: A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meaf.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meaf.s	⊢ 𝑆 = dom 𝑀
Assertion	meaf	⊢ ( 𝜑 → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		meaf.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meaf.s	⊢ 𝑆 = dom 𝑀
3		ismea	⊢ ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
4	1 3	sylib	⊢ ( 𝜑 → ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
5	4	simpld	⊢ ( 𝜑 → ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) )
6	5	simplld	⊢ ( 𝜑 → 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) )
7	2	a1i	⊢ ( 𝜑 → 𝑆 = dom 𝑀 )
8	7	feq2d	⊢ ( 𝜑 → ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ↔ 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ) )
9	6 8	mpbird	⊢ ( 𝜑 → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )