Metamath Proof Explorer

Theorem measvxrge0

Description: The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016)

Ref Expression
Assertion measvxrge0 ⊢ M ∈ measures ⁡ S ∧ A ∈ S → M ⁡ A ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 measfrge0 ⊢ M ∈ measures ⁡ S → M : S ⟶ 0 +∞
2 1 ffvelrnda ⊢ M ∈ measures ⁡ S ∧ A ∈ S → M ⁡ A ∈ 0 +∞