Theorem dfarea

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

	Ref	Expression
Assertion	dfarea	$$⊢area=\left(s\in \mathrm{dom}area⟼{\int }_{ℝ}vol\left(s\left[\left\{x\right\}\right]\right)dx\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-area	$$⊢area=\left(s\in \left\{y\in 𝒫{ℝ}^2|\left(\forall x\in ℝy\left[\left\{x\right\}\right]\in {vol}^{-1}\left[ℝ\right]\wedge \left(x\in ℝ⟼vol\left(y\left[\left\{x\right\}\right]\right)\right)\in {𝐿}^1\right)\right\}⟼{\int }_{ℝ}vol\left(s\left[\left\{x\right\}\right]\right)dx\right)$$
2		itgex	$$⊢{\int }_{ℝ}vol\left(s\left[\left\{x\right\}\right]\right)dx\in \mathrm{V}$$
3	2 1	dmmpti	$$⊢\mathrm{dom}area=\left\{y\in 𝒫{ℝ}^2|\left(\forall x\in ℝy\left[\left\{x\right\}\right]\in {vol}^{-1}\left[ℝ\right]\wedge \left(x\in ℝ⟼vol\left(y\left[\left\{x\right\}\right]\right)\right)\in {𝐿}^1\right)\right\}$$
4	3	mpteq1i	$$⊢\left(s\in \mathrm{dom}area⟼{\int }_{ℝ}vol\left(s\left[\left\{x\right\}\right]\right)dx\right)=\left(s\in \left\{y\in 𝒫{ℝ}^2|\left(\forall x\in ℝy\left[\left\{x\right\}\right]\in {vol}^{-1}\left[ℝ\right]\wedge \left(x\in ℝ⟼vol\left(y\left[\left\{x\right\}\right]\right)\right)\in {𝐿}^1\right)\right\}⟼{\int }_{ℝ}vol\left(s\left[\left\{x\right\}\right]\right)dx\right)$$
5	1 4	eqtr4i	$$⊢area=\left(s\in \mathrm{dom}area⟼{\int }_{ℝ}vol\left(s\left[\left\{x\right\}\right]\right)dx\right)$$