Metamath Proof Explorer

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 ⊢ M ∈ measures ⁡ S → M : S ⟶ 0 +∞

Proof

Step Hyp Ref Expression
1 measbase ⊢ M ∈ measures ⁡ S → S ∈ ⋃ ran ⁡ sigAlgebra
2 ismeas ⊢ S ∈ ⋃ ran ⁡ sigAlgebra → M ∈ measures ⁡ S ↔ M : S ⟶ 0 +∞ ∧ M ⁡ ∅ = 0 ∧ ∀ y ∈ 𝒫 S y ≼ ω ∧ Disj x ∈ y x → M ⁡ ⋃ y = ∑ * x ∈ y M ⁡ x
3 1 2 syl ⊢ M ∈ measures ⁡ S → M ∈ measures ⁡ S ↔ M : S ⟶ 0 +∞ ∧ M ⁡ ∅ = 0 ∧ ∀ y ∈ 𝒫 S y ≼ ω ∧ Disj x ∈ y x → M ⁡ ⋃ y = ∑ * x ∈ y M ⁡ x
4 3 ibi ⊢ M ∈ measures ⁡ S → M : S ⟶ 0 +∞ ∧ M ⁡ ∅ = 0 ∧ ∀ y ∈ 𝒫 S y ≼ ω ∧ Disj x ∈ y x → M ⁡ ⋃ y = ∑ * x ∈ y M ⁡ x
5 4 simp1d ⊢ M ∈ measures ⁡ S → M : S ⟶ 0 +∞