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 ffvelcdmi ⊢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