Metamath Proof Explorer

Theorem dmarea

Description: The domain of the area function is the set of finitely measurable subsets of RR X. RR . (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion dmarea ⊢A∈dom⁡area↔A⊆ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1

Proof

Step Hyp Ref Expression
1 itgex ⊢∫ℝvol⁡sxdx∈V
2 df-area ⊢area=s∈t∈𝒫ℝ2|∀x∈ℝtx∈vol-1ℝ∧x∈ℝ⟼vol⁡tx∈𝐿1⟼∫ℝvol⁡sxdx
3 1 2 dmmpti ⊢dom⁡area=t∈𝒫ℝ2|∀x∈ℝtx∈vol-1ℝ∧x∈ℝ⟼vol⁡tx∈𝐿1
4 3 eleq2i ⊢A∈dom⁡area↔A∈t∈𝒫ℝ2|∀x∈ℝtx∈vol-1ℝ∧x∈ℝ⟼vol⁡tx∈𝐿1
5 imaeq1 ⊢t=A→tx=Ax
6 5 eleq1d ⊢t=A→tx∈vol-1ℝ↔Ax∈vol-1ℝ
7 6 ralbidv ⊢t=A→∀x∈ℝtx∈vol-1ℝ↔∀x∈ℝAx∈vol-1ℝ
8 5 fveq2d ⊢t=A→vol⁡tx=vol⁡Ax
9 8 mpteq2dv ⊢t=A→x∈ℝ⟼vol⁡tx=x∈ℝ⟼vol⁡Ax
10 9 eleq1d ⊢t=A→x∈ℝ⟼vol⁡tx∈𝐿1↔x∈ℝ⟼vol⁡Ax∈𝐿1
11 7 10 anbi12d ⊢t=A→∀x∈ℝtx∈vol-1ℝ∧x∈ℝ⟼vol⁡tx∈𝐿1↔∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1
12 11 elrab ⊢A∈t∈𝒫ℝ2|∀x∈ℝtx∈vol-1ℝ∧x∈ℝ⟼vol⁡tx∈𝐿1↔A∈𝒫ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1
13 reex ⊢ℝ∈V
14 13 13 xpex ⊢ℝ2∈V
15 14 elpw2 ⊢A∈𝒫ℝ2↔A⊆ℝ2
16 15 anbi1i ⊢A∈𝒫ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1↔A⊆ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1
17 3anass ⊢A⊆ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1↔A⊆ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1
18 16 17 bitr4i ⊢A∈𝒫ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1↔A⊆ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1
19 4 12 18 3bitri ⊢A∈dom⁡area↔A⊆ℝ2∧∀x∈ℝAx∈vol-1ℝ∧x∈ℝ⟼vol⁡Ax∈𝐿1