Definition df-area 26087

Description: Define the area of a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.)

Assertion

Ref	Expression
df-area	⊢ area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)

Distinct variable group:   𝑡,𝑠,𝑥

Detailed syntax breakdown of Definition df-area

Step	Hyp	Ref	Expression
1		carea 26086	. 2 class area
2		vs	. . 3 setvar 𝑠
3		vt	. . . . . . . . 9 setvar 𝑡
4	3	cv 1540	. . . . . . . 8 class 𝑡
5		vx	. . . . . . . . . 10 setvar 𝑥
6	5	cv 1540	. . . . . . . . 9 class 𝑥
7	6	csn 4566	. . . . . . . 8 class {𝑥}
8	4, 7	cima 5591	. . . . . . 7 class (𝑡 “ {𝑥})
9		cvol 24608	. . . . . . . . 9 class vol
10	9	ccnv 5587	. . . . . . . 8 class ◡vol
11		cr 10854	. . . . . . . 8 class ℝ
12	10, 11	cima 5591	. . . . . . 7 class (◡vol “ ℝ)
13	8, 12	wcel 2109	. . . . . 6 wff (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ)
14	13, 5, 11	wral 3065	. . . . 5 wff ∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ)
15	8, 9	cfv 6430	. . . . . . 7 class (vol‘(𝑡 “ {𝑥}))
16	5, 11, 15	cmpt 5161	. . . . . 6 class (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥})))
17		cibl 24762	. . . . . 6 class 𝐿1
18	16, 17	wcel 2109	. . . . 5 wff (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1
19	14, 18	wa 395	. . . 4 wff (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)
20	11, 11	cxp 5586	. . . . 5 class (ℝ × ℝ)
21	20	cpw 4538	. . . 4 class 𝒫 (ℝ × ℝ)
22	19, 3, 21	crab 3069	. . 3 class {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)}
23	2	cv 1540	. . . . . 6 class 𝑠
24	23, 7	cima 5591	. . . . 5 class (𝑠 “ {𝑥})
25	24, 9	cfv 6430	. . . 4 class (vol‘(𝑠 “ {𝑥}))
26	5, 11, 25	citg 24763	. . 3 class ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥
27	2, 22, 26	cmpt 5161	. 2 class (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
28	1, 27	wceq 1541	1 wff area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)

This definition is referenced by:  dmarea  26088  dfarea  26091