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 e. dom area -> ( area ` S ) e. RR )

Proof

Step Hyp Ref Expression
1 areaf
 |-  area : dom area --> ( 0 [,) +oo )
2 1 ffvelrni
 |-  ( S e. dom area -> ( area ` S ) e. ( 0 [,) +oo ) )
3 elrege0
 |-  ( ( area ` S ) e. ( 0 [,) +oo ) <-> ( ( area ` S ) e. RR /\ 0 <_ ( area ` S ) ) )
4 3 simplbi
 |-  ( ( area ` S ) e. ( 0 [,) +oo ) -> ( area ` S ) e. RR )
5 2 4 syl
 |-  ( S e. dom area -> ( area ` S ) e. RR )