Theorem areaval

Description: The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	areaval	|- ( S e. dom area -> ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( s = S /\ x e. RR ) -> s = S )
2	1	imaeq1d	|- ( ( s = S /\ x e. RR ) -> ( s " { x } ) = ( S " { x } ) )
3	2	fveq2d	|- ( ( s = S /\ x e. RR ) -> ( vol ` ( s " { x } ) ) = ( vol ` ( S " { x } ) ) )
4	3	itgeq2dv	|- ( s = S -> S. RR ( vol ` ( s " { x } ) ) _d x = S. RR ( vol ` ( S " { x } ) ) _d x )
5		dfarea	|- area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )
6		itgex	|- S. RR ( vol ` ( S " { x } ) ) _d x e. _V
7	4 5 6	fvmpt	|- ( S e. dom area -> ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x )