Theorem dfarea

Description: Rewrite df-area self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	dfarea	⊢ area = ( 𝑠 ∈ dom area ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		df-area	⊢ area = ( 𝑠 ∈ { 𝑦 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑦 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑦 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )
2		itgex	⊢ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 ∈ V
3	2 1	dmmpti	⊢ dom area = { 𝑦 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑦 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑦 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) }
4	3	mpteq1i	⊢ ( 𝑠 ∈ dom area ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 ) = ( 𝑠 ∈ { 𝑦 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑦 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑦 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )
5	1 4	eqtr4i	⊢ area = ( 𝑠 ∈ dom area ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )