Metamath Proof Explorer

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 ⊢φ→M∈Meas
meaf.s ⊢S=dom⁡M
Assertion meaf ⊢φ→M:S⟶0+∞

Proof

Step Hyp Ref Expression
1 meaf.m ⊢φ→M∈Meas
2 meaf.s ⊢S=dom⁡M
3 ismea ⊢M∈Meas↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
4 1 3 sylib ⊢φ→M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
5 4 simpld ⊢φ→M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0
6 5 simplld ⊢φ→M:dom⁡M⟶0+∞
7 2 a1i ⊢φ→S=dom⁡M
8 7 feq2d ⊢φ→M:S⟶0+∞↔M:dom⁡M⟶0+∞
9 6 8 mpbird ⊢φ→M:S⟶0+∞