Theorem dmarea 26442

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

Assertion

Ref	Expression
dmarea	⊢ (𝐴 ∈ dom area ↔ (𝐴 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1))

Distinct variable group:   𝑥,𝐴

Proof of Theorem dmarea

Dummy variables 𝑡 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		itgex 25270	. . . 4 ⊢ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥 ∈ V
2		df-area 26441	. . . 4 ⊢ area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
3	1, 2	dmmpti 6691	. . 3 ⊢ dom area = {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)}
4	3	eleq2i 2826	. 2 ⊢ (𝐴 ∈ dom area ↔ 𝐴 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)})
5		imaeq1 6052	. . . . . 6 ⊢ (𝑡 = 𝐴 → (𝑡 “ {𝑥}) = (𝐴 “ {𝑥}))
6	5	eleq1d 2819	. . . . 5 ⊢ (𝑡 = 𝐴 → ((𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ↔ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ)))
7	6	ralbidv 3178	. . . 4 ⊢ (𝑡 = 𝐴 → (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ↔ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ)))
8	5	fveq2d 6892	. . . . . 6 ⊢ (𝑡 = 𝐴 → (vol‘(𝑡 “ {𝑥})) = (vol‘(𝐴 “ {𝑥})))
9	8	mpteq2dv 5249	. . . . 5 ⊢ (𝑡 = 𝐴 → (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) = (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))))
10	9	eleq1d 2819	. . . 4 ⊢ (𝑡 = 𝐴 → ((𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1 ↔ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1))
11	7, 10	anbi12d 632	. . 3 ⊢ (𝑡 = 𝐴 → ((∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1) ↔ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1)))
12	11	elrab 3682	. 2 ⊢ (𝐴 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↔ (𝐴 ∈ 𝒫 (ℝ × ℝ) ∧ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1)))
13		reex 11197	. . . . . 6 ⊢ ℝ ∈ V
14	13, 13	xpex 7735	. . . . 5 ⊢ (ℝ × ℝ) ∈ V
15	14	elpw2 5344	. . . 4 ⊢ (𝐴 ∈ 𝒫 (ℝ × ℝ) ↔ 𝐴 ⊆ (ℝ × ℝ))
16	15	anbi1i 625	. . 3 ⊢ ((𝐴 ∈ 𝒫 (ℝ × ℝ) ∧ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1)) ↔ (𝐴 ⊆ (ℝ × ℝ) ∧ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1)))
17		3anass 1096	. . 3 ⊢ ((𝐴 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1) ↔ (𝐴 ⊆ (ℝ × ℝ) ∧ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1)))
18	16, 17	bitr4i 278	. 2 ⊢ ((𝐴 ∈ 𝒫 (ℝ × ℝ) ∧ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1)) ↔ (𝐴 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1))
19	4, 12, 18	3bitri 297	1 ⊢ (𝐴 ∈ dom area ↔ (𝐴 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1))

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ∀wral 3062  {crab 3433   ⊆ wss 3947  𝒫 cpw 4601  {csn 4627   ↦ cmpt 5230   × cxp 5673  ^◡ccnv 5674  dom cdm 5675   “ cima 5678  ‘cfv 6540  ℝcr 11105  volcvol 24962  𝐿¹cibl 25116  ∫citg 25117  areacarea 26440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-fv 6548  df-sum 15629  df-itg 25122  df-area 26441

This theorem is referenced by:  areambl  26443  areass  26444  areaf  26446  areacirc  36519  arearect  41897  areaquad  41898