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