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	⊢ ( 𝑆 ∈ dom area → ( area ‘ 𝑆 ) = ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑥 ∈ ℝ ) → 𝑠 = 𝑆 )
2	1	imaeq1d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑥 ∈ ℝ ) → ( 𝑠 “ { 𝑥 } ) = ( 𝑆 “ { 𝑥 } ) )
3	2	fveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑥 ∈ ℝ ) → ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) = ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) )
4	3	itgeq2dv	⊢ ( 𝑠 = 𝑆 → ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 = ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥 )
5		dfarea	⊢ area = ( 𝑠 ∈ dom area ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )
6		itgex	⊢ ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥 ∈ V
7	4 5 6	fvmpt	⊢ ( 𝑆 ∈ dom area → ( area ‘ 𝑆 ) = ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥 )