Metamath Proof Explorer

Theorem areage0

Description: The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areage0 ⊢ S ∈ dom ⁡ area → 0 ≤ area ⁡ S

Proof

Step Hyp Ref Expression
1 areaf ⊢ area : dom ⁡ area ⟶ 0 +∞
2 1 ffvelrni ⊢ S ∈ dom ⁡ area → area ⁡ S ∈ 0 +∞
3 elrege0 ⊢ area ⁡ S ∈ 0 +∞ ↔ area ⁡ S ∈ ℝ ∧ 0 ≤ area ⁡ S
4 3 simprbi ⊢ area ⁡ S ∈ 0 +∞ → 0 ≤ area ⁡ S
5 2 4 syl ⊢ S ∈ dom ⁡ area → 0 ≤ area ⁡ S