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 ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
4 1 3 sylib ⊢ φ → M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → 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 +∞