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 ∈ ℝ A x ∈ vol -1 ℝ ∧ x ∈ ℝ ⟼ vol ⁡ A x ∈ 𝐿 1

Proof

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