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	ffvelcdmi	|- ( 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 )