Metamath Proof Explorer

Theorem areacl

Description: The area of a measurable region is a real number. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areacl ⊢S∈dom⁡area→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 simplbi ⊢area⁡S∈0+∞→area⁡S∈ℝ
5 2 4 syl ⊢S∈dom⁡area→area⁡S∈ℝ